1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Finite types.
  7  -/
  8  import data.finset algebra.big_operators data.array.lemmas logic.unique
src         └─────────┘ └───────────────────┘ └───────────────┘ └──────────┘
  9  import tactic.wlog
src         └─────────┘
 10  universes u v
 11  
 12  variables {α : Type*} {β : Type*} {γ : Type*}
 13  
 14  /-- `fintype α` means that `α` is finite, i.e. there are only
 15    finitely many distinct elements of type `α`. The evidence of this
 16    is a finset `elems` (a list up to permutation without duplicates),
 17    together with a proof that everything of type `α` is in the list. -/
 18  class fintype (α : Type*) :=
id                      └───┘
typ                     └───┘
 19  (elems : finset α)
id            └────┘ 
src           └────┘
typ           └────┘ 
doc           └────┘
 20  (complete : ∀ x : α, x ∈ elems)
id                        └───┘
src                         
typ                       └───┘
 21  
 22  namespace finset
 23  variable [fintype α]
id             └─────┘
src            └─────┘
typ            └─────┘
doc            └─────┘
 24  
 25  /-- `univ` is the universal finite set of type `finset α` implied from
 26    the assumption `fintype α`. -/
 27  def univ : finset α := fintype.elems α
id              └────┘     └───────────┘ 
src             └────┘      └───────────┘
typ             └────┘     └───────────┘ 
doc             └────┘
 28  
 29  @[simp] theorem mem_univ (x : α) : x ∈ (univ : finset α) :=
id                                        └──┘   └────┘ 
src                                         └──┘   └────┘
typ                                       └──┘   └────┘ 
doc    └──┘                                  └──┘   └────┘
 30  fintype.complete x
id   └──────────────┘ 
src  └──────────────┘
typ  └──────────────┘ 
 31  
 32  @[simp] theorem mem_univ_val : ∀ x, x ∈ (univ : finset α).1 := mem_univ
id                                         └──┘   └────┘       └──────┘
src                                          └──┘   └────┘        └──────┘
typ                                        └──┘   └────┘       └──────┘
doc    └──┘                                   └──┘   └────┘
 33  
 34  @[simp] lemma coe_univ : ↑(univ : finset α) = (set.univ : set α) :=
id                             └──┘   └────┘     └──────┘   └─┘ 
src                            └──┘   └────┘      └──────┘   └─┘
typ                            └──┘   └────┘     └──────┘   └─┘ 
doc    └──┘                     └──┘   └────┘
 35  by ext; simp
src     └─┘  └────
typ     └─┘  └────
doc     └─┘  └────
txt     └─┘  └────
par     └─┘  └────
pid              
st     └──────────
 36  
src  
typ  
doc  
txt  
par  
pid  
st   
 37  theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
id                            └────┘       └──┘         └──────┘ 
src                           └────┘         └──┘           └──────┘
typ                           └────┘       └──┘         └──────┘ 
doc                           └────┘          └──┘
 38  
 39  theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
id                                   └────┘       └──┘        
src                                  └────┘         └──┘         
typ                                  └────┘       └──┘        
doc                                  └────┘          └──┘
 40  by simp [ext]
id            └─┘
src     └────┘└─┘└─
typ     └────┘└─┘└─
doc     └────┘   └─
txt     └────┘   └─
par     └────┘   └─
pid            
st     └───────────
 41  
src  
typ  
doc  
txt  
par  
pid  
st   
 42  @[simp] lemma piecewise_univ [∀i : α, decidable (i ∈ (univ : finset α))]
id                                        └───────┘     └──┘   └────┘ 
src                                        └───────┘      └──┘   └────┘
typ                                       └───────┘     └──┘   └────┘ 
doc    └──┘                                                └──┘   └────┘
 43    {δ : α → Sort*} (f g : Πi, δ i) : univ.piecewise f g = f :=
id                                   └──┘└────────┘    
src                                      └──┘└────────┘     
typ                                  └──┘└────────┘    
doc                                      └──┘└────────┘
 44  by { ext i, simp [piecewise] }
id                     └───────┘
src       └───┘  └────┘└───────┘└┘
typ       └───┘  └────┘└───────┘└┘
doc       └───┘  └────┘└───────┘└┘
txt       └───┘  └────┘         └┘
par       └───┘  └────┘         └┘
pid          └┘               
st     └──────┘└─────────────────┘└┘
 45  
 46  end finset
 47  
 48  open finset function
 49  
 50  namespace fintype
 51  
 52  instance decidable_pi_fintype {α} {β : α → Type*} [fintype α] [∀a, decidable_eq (β a)] :
id                                                     └─────┘       └──────────┘   
src                                                     └─────┘         └──────────┘
typ                                                    └─────┘       └──────────┘   
doc                                                     └─────┘
 53    decidable_eq (Πa, β a) :=
id     └──────────┘      
src    └──────────┘
typ    └──────────┘      
 54  assume f g, decidable_of_iff (∀ a ∈ fintype.elems α, f a = g a)
id             └──────────────┘       └───────────┘       
src              └──────────────┘       └───────────┘        
typ            └──────────────┘       └───────────┘       
 55    (by simp [function.funext_iff, fintype.complete])
id               └─────────────────┘  └──────────────┘
src        └────┘└─────────────────┘└┘└──────────────┘
typ        └────┘└─────────────────┘└┘└──────────────┘
doc        └────┘                   └┘                
txt        └────┘                   └┘                
par        └────┘                   └┘                
pid                               └┘                
st        └───────────────────────────────────────────┘
 56  
 57  instance decidable_forall_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
id                                      └─────┘                  └────────────┘ 
src                                     └─────┘                    └────────────┘
typ                                     └─────┘                  └────────────┘ 
doc                                     └─────┘
 58    decidable (∀ a, p a) :=
id     └───────┘       
src    └───────┘
typ    └───────┘       
 59  decidable_of_iff (∀ a ∈ @univ α _, p a) (by simp)
id   └──────────────┘        └──┘      
src  └──────────────┘         └──┘               └──┘
typ  └──────────────┘        └──┘            └──┘
doc                           └──┘               └──┘
txt                                              └──┘
par                                              └──┘
st                                              └───┘
 60  
 61  instance decidable_exists_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
id                                      └─────┘                  └────────────┘ 
src                                     └─────┘                    └────────────┘
typ                                     └─────┘                  └────────────┘ 
doc                                     └─────┘
 62    decidable (∃ a, p a) :=
id     └───────┘     
src    └───────┘    
typ    └───────┘     
 63  decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
id   └──────────────┘       └──┘     
src  └──────────────┘        └──┘              └──┘
typ  └──────────────┘       └──┘           └──┘
doc                           └──┘               └──┘
txt                                              └──┘
par                                              └──┘
st                                              └───┘
 64  
 65  instance decidable_eq_equiv_fintype [fintype α] [decidable_eq β] :
id                                        └─────┘    └──────────┘ 
src                                       └─────┘     └──────────┘
typ                                       └─────┘    └──────────┘ 
doc                                       └─────┘
 66    decidable_eq (α ≃ β) :=
id     └──────────┘    
src    └──────────┘    
typ    └──────────┘    
doc                    
 67  λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext _ _ (congr_fun h), congr_arg _⟩
id        └──────────────┘             └───────┘      └───────┘    └───────┘
src         └──────────────┘                └───────┘      └───────┘     └───────┘
typ       └──────────────┘             └───────┘      └───────┘    └───────┘
 68  
 69  instance decidable_injective_fintype [fintype α] [decidable_eq α] [decidable_eq β] :
id                                         └─────┘    └──────────┘    └──────────┘ 
src                                        └─────┘     └──────────┘     └──────────┘
typ                                        └─────┘    └──────────┘    └──────────┘ 
doc                                        └─────┘
 70    decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
id     └────────────┘  └───────┘                     
src    └────────────┘  └───────┘                              └──────────────┘  └──────────────
typ    └────────────┘  └───────┘                          └──────────────┘  └──────────────
doc                                                           └──────────────┘  └──────────────
txt                                                           └──────────────┘  └──────────────
par                                                           └──────────────┘  └──────────────
pid                                                                 └────────┘                
st                                                           └─────────────────────────────────
 71  
src  
typ  
doc  
txt  
par  
pid  
st   
 72  instance decidable_surjective_fintype [fintype α] [fintype β] [decidable_eq β] :
id                                          └─────┘    └─────┘    └──────────┘ 
src                                         └─────┘     └─────┘     └──────────┘
typ                                         └─────┘    └─────┘    └──────────┘ 
doc                                         └─────┘     └─────┘
 73    decidable_pred (surjective : (α → β) → Prop) := λ x, by unfold surjective; apply_instance
id     └────────────┘  └────────┘                     
src    └────────────┘  └────────┘                              └───────────────┘  └──────────────
typ    └────────────┘  └────────┘                          └───────────────┘  └──────────────
doc                                                            └───────────────┘  └──────────────
txt                                                            └───────────────┘  └──────────────
par                                                            └───────────────┘  └──────────────
pid                                                                  └─────────┘                
st                                                            └──────────────────────────────────
 74  
src  
typ  
doc  
txt  
par  
pid  
st   
 75  instance decidable_bijective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
id                                         └─────┘    └──────────┘    └─────┘    └──────────┘ 
src                                        └─────┘     └──────────┘     └─────┘     └──────────┘
typ                                        └─────┘    └──────────┘    └─────┘    └──────────┘ 
doc                                        └─────┘                      └─────┘
 76    decidable_pred (bijective : (α → β) → Prop) := λ x, by unfold bijective; apply_instance
id     └────────────┘  └───────┘                     
src    └────────────┘  └───────┘                              └──────────────┘  └──────────────
typ    └────────────┘  └───────┘                          └──────────────┘  └──────────────
doc                                                           └──────────────┘  └──────────────
txt                                                           └──────────────┘  └──────────────
par                                                           └──────────────┘  └──────────────
pid                                                                 └────────┘                
st                                                           └─────────────────────────────────
 77  
src  
typ  
doc  
txt  
par  
pid  
st   
 78  instance decidable_left_inverse_fintype [fintype α] [decidable_eq α] (f : α → β) (g : β → α) :
id                                            └─────┘    └──────────┘                     
src                                           └─────┘     └──────────┘
typ                                           └─────┘    └──────────┘                     
doc                                           └─────┘
 79    decidable (function.right_inverse f g) :=
id     └───────┘  └────────────────────┘  
src    └───────┘  └────────────────────┘
typ    └───────┘  └────────────────────┘  
 80  show decidable (∀ x, g (f x) = x), by apply_instance
id        └───────┘            
src       └───────┘                       └──────────────
typ       └───────┘                  └──────────────
doc                                        └──────────────
txt                                        └──────────────
par                                        └──────────────
pid                                                      
st                                        └───────────────
 81  
src  
typ  
doc  
txt  
par  
pid  
st   
 82  instance decidable_right_inverse_fintype [fintype β] [decidable_eq β] (f : α → β) (g : β → α) :
id                                             └─────┘    └──────────┘                     
src                                            └─────┘     └──────────┘
typ                                            └─────┘    └──────────┘                     
doc                                            └─────┘
 83    decidable (function.left_inverse f g) :=
id     └───────┘  └───────────────────┘  
src    └───────┘  └───────────────────┘
typ    └───────┘  └───────────────────┘  
 84  show decidable (∀ x, f (g x) = x), by apply_instance
id        └───────┘            
src       └───────┘                       └──────────────
typ       └───────┘                  └──────────────
doc                                        └──────────────
txt                                        └──────────────
par                                        └──────────────
pid                                                      
st                                        └───────────────
 85  
src  
typ  
doc  
txt  
par  
pid  
st   
 86  /-- Construct a proof of `fintype α` from a universal multiset -/
 87  def of_multiset [decidable_eq α] (s : multiset α)
id                    └──────────┘        └──────┘ 
src                   └──────────┘         └──────┘
typ                   └──────────┘        └──────┘ 
doc                                        └──────┘
 88    (H : ∀ x : α, x ∈ s) : fintype α :=
id                        └─────┘ 
src                          └─────┘
typ                       └─────┘ 
doc                           └─────┘
 89  ⟨s.to_finset, by simpa using H⟩
id    └────────┘                 
src    └────────┘     └──────────┘
typ   └────────┘     └──────────┘
doc    └────────┘     └──────────┘
txt                   └──────────┘
par                   └──────────┘
pid                        └────┘
st                   └────────────┘
 90  
 91  /-- Construct a proof of `fintype α` from a universal list -/
 92  def of_list [decidable_eq α] (l : list α)
id                └──────────┘        └──┘ 
src               └──────────┘         └──┘
typ               └──────────┘        └──┘ 
 93    (H : ∀ x : α, x ∈ l) : fintype α :=
id                        └─────┘ 
src                          └─────┘
typ                       └─────┘ 
doc                           └─────┘
 94  ⟨l.to_finset, by simpa using H⟩
id    └────────┘                 
src    └────────┘     └──────────┘
typ   └────────┘     └──────────┘
doc    └────────┘     └──────────┘
txt                   └──────────┘
par                   └──────────┘
pid                        └────┘
st                   └────────────┘
 95  
 96  theorem exists_univ_list (α) [fintype α] :
id                                 └─────┘ 
src                                └─────┘
typ                                └─────┘ 
doc                                └─────┘
 97    ∃ l : list α, l.nodup ∧ ∀ x : α, x ∈ l :=
id          └──┘  └────┘            
src         └──┘    └────┘             
typ         └──┘  └────┘            
doc                   └────┘
 98  let ⟨l, e⟩ := quotient.exists_rep (@univ α _).1 in
id   └─┘           └─────────────────┘   └──┘    
src                └─────────────────┘   └──┘     
typ  └─┘           └─────────────────┘   └──┘    
doc                                      └──┘
 99  by have := and.intro univ.2 mem_univ_val;
id              └───────┘ └──┘   └──────────┘
src     └──────┘└───────┘└──┘└─┘└──────────┘
typ     └──────┘└───────┘└──┘└─┘└──────────┘
doc     └──────┘         └──┘└─┘
txt     └──────┘             └─┘
par     └──────┘             └─┘
pid     └───┘└─┘             └─┘
st     └───────────────────────────────────────
100     exact ⟨_, by rwa ← e at this⟩
id                         
src     └────┘ └─┘  └────┘ └──────┘└─
typ     └────┘ └─┘  └────┘└──────┘└─
doc     └────┘ └─┘  └────┘ └──────┘└─
txt     └────┘ └─┘  └────┘ └──────┘└─
par     └────┘ └─┘  └────┘ └──────┘└─
pid           └─┘  └─────┘ └───────┘
st   ──────────────┘└──────────────┘└─
101  
src  
typ  
doc  
txt  
par  
pid  
st   
102  /-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
103  def card (α) [fintype α] : ℕ := (@univ α _).card
id                 └─────┘           └──┘    └──┘
src                └─────┘            └──┘     └──┘
typ                └─────┘           └──┘    └──┘
doc                └─────┘             └──┘     └──┘
104  
105  /-- If `l` lists all the elements of `α` without duplicates, then `α ≃ fin (l.length)`. -/
106  def equiv_fin_of_forall_mem_list {α} [decidable_eq α]
id                                         └──────────┘ 
src                                        └──────────┘
typ                                        └──────────┘ 
107    {l : list α} (h : ∀ x:α, x ∈ l) (nd : l.nodup) : α ≃ fin (l.length) :=
id          └──┘                        └────┘      └─┘  └─────┘
src         └──┘                             └────┘       └─┘   └─────┘
typ         └──┘                        └────┘      └─┘  └─────┘
doc                                           └────┘      
108  ⟨λ a, ⟨_, list.index_of_lt_length.2 (h a)⟩,
id            └─────────────────────┘    
src            └─────────────────────┘
typ           └─────────────────────┘    
109   λ i, l.nth_le i.1 i.2,
id        └─────┘   
src         └─────┘     
typ       └─────┘   
110   λ a, by simp,
id      
src           └──┘
typ          └──┘
doc           └──┘
txt           └──┘
par           └──┘
st           └───┘
111   λ ⟨i, h⟩, fin.eq_of_veq $ list.nodup_iff_nth_le_inj.1 nd _ _
id            └───────────┘   └───────────────────────┘  └┘
src             └───────────┘   └───────────────────────┘
typ           └───────────┘   └───────────────────────┘  └┘
112     (list.index_of_lt_length.2 (list.nth_le_mem _ _ _)) h $ by simp⟩
id       └─────────────────────┘   └─────────────┘
src      └─────────────────────┘   └─────────────┘                └──┘
typ      └─────────────────────┘   └─────────────┘                └──┘
doc                                                                └──┘
txt                                                                └──┘
par                                                                └──┘
st                                                                └───┘
113  
114  /-- There is (computably) a bijection between `α` and `fin n` where
115    `n = card α`. Since it is not unique, and depends on which permutation
116    of the universe list is used, the bijection is wrapped in `trunc` to
117    preserve computability.  -/
118  def equiv_fin (α) [fintype α] [decidable_eq α] : trunc (α ≃ fin (card α)) :=
id                      └─────┘    └──────────┘     └───┘    └─┘  └──┘ 
src                     └─────┘     └──────────┘      └───┘     └─┘  └──┘
typ                     └─────┘    └──────────┘     └───┘    └─┘  └──┘ 
doc                     └─────┘                       └───┘          └──┘
119  by unfold card finset.card; exact
src     └─────────────────────┘  └────┘
typ     └─────────────────────┘  └────┘
doc     └─────────────────────┘  └────┘
txt     └─────────────────────┘  └────┘
par     └─────────────────────┘  └────┘
pid           └───────────────┘       
st     └───────────────────────────────
120  quot.rec_on_subsingleton (@univ α _).1
id   └──────────────────────┘
src  └──────────────────────┘       └─────
typ  └──────────────────────┘       └─────
doc                                 └─────
txt                                 └─────
par                                 └─────
pid                                 └─────
st   ───────────────────────────────────────
121    (λ l (h : ∀ x:α, x ∈ l) (nd : l.nodup), trunc.mk (equiv_fin_of_forall_mem_list h nd))
id                                  └────┘   └──────┘  └──────────────────────────┘
src  ─┘  └──────┘ └─┘    └──────┘ └────┘└─┘└──────┘ └──────────────────────────┘   └──
typ  ─┘  └──────┘ └─┘   └──────┘ └────┘└─┘└──────┘ └──────────────────────────┘   └──
doc  ─┘  └──────┘ └─┘     └──────┘ └────┘└─┘└──────┘ └──────────────────────────┘   └──
txt  ─┘  └──────┘ └─┘     └──────┘       └─┘                                        └──
par  ─┘  └──────┘ └─┘     └──────┘       └─┘                                        └──
pid  ─┘  └──────┘ └─┘     └──────┘       └─┘                                        └──
st   ────────────────────────────────────────────────────────────────────────────────────────
122    mem_univ_val univ.2
id     └──────────┘ └──┘
src  ─┘└──────────┘└──┘└──
typ  ─┘└──────────┘└──┘└──
doc  ─┘            └──┘└──
txt  ─┘                └──
par  ─┘                └──
pid  ─┘                └──
st   ──────────────────────
123  
src  
typ  
doc  
txt  
par  
pid  
st   
124  theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
id                                 └─────┘       └──────┘    └─┘ 
src                                └─────┘         └──────┘     └─┘
typ                                └─────┘       └──────┘    └─┘ 
doc                                └─────┘                       
125  by haveI := classical.dec_eq α; exact ⟨card α, nonempty_of_trunc (equiv_fin α)⟩
id               └──────────────┘          └──┘    └───────────────┘  └───────┘ 
src     └───────┘└──────────────┘   └────┘ └──┘ └┘└───────────────┘ └───────┘ └──
typ     └───────┘└──────────────┘  └────┘ └──┘ └┘└───────────────┘ └───────┘└──
doc     └───────┘                   └────┘ └──┘ └┘                  └───────┘ └──
txt     └───────┘                   └────┘      └┘                            └──
par     └───────┘                   └────┘      └┘                            └──
pid          └─┘                              └┘                            └┘
st     └─────────────────────────────────────────────────────────────────────────────
126  
src  
typ  
doc  
txt  
par  
pid  
st   
127  instance (α : Type*) : subsingleton (fintype α) :=
id                          └──────────┘  └─────┘ 
src                         └──────────┘  └─────┘
typ                         └──────────┘  └─────┘ 
doc                                       └─────┘
128  ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext, h₁, h₂]⟩
id                                       └────────┘  └┘  └┘
src                           └───┘  └────┘└────────┘└┘  └┘  
typ                         └───┘  └────┘└────────┘└┘└┘└┘└┘
doc                                  └────┘          └┘  └┘  
txt                           └───┘  └────┘          └┘  └┘  
par                           └───┘  └────┘          └┘  └┘  
pid                                                └┘  └┘  
st                           └───────────────────────────────┘
129  
130  protected def subtype {p : α → Prop} (s : finset α)
id                                            └────┘ 
src                                            └────┘
typ                                           └────┘ 
doc                                            └────┘
131    (H : ∀ x : α, x ∈ s ↔ p x) : fintype {x // p x} :=
id                           └─────┘      
src                               └─────┘ 
typ                          └─────┘      
doc                                 └─────┘
132  ⟨⟨multiset.pmap subtype.mk s.1 (λ x, (H x).1),
id     └───────────┘ └────────┘           
src    └───────────┘ └────────┘               
typ    └───────────┘ └────────┘           
doc    └───────────┘
133    multiset.nodup_pmap (λ a _ b _, congr_arg subtype.val) s.2⟩,
id     └─────────────────┘         └───────┘ └─────────┘  
src    └─────────────────┘             └───────┘ └─────────┘   
typ    └─────────────────┘         └───────┘ └─────────┘  
134  λ ⟨x, px⟩, multiset.mem_pmap.2 ⟨x, (H x).2 px, rfl⟩⟩
id       └┘   └───────────────┘                └─┘
src             └───────────────┘                 └─┘
typ      └┘   └───────────────┘                └─┘
135  
136  theorem subtype_card {p : α → Prop} (s : finset α)
id                                           └────┘ 
src                                           └────┘
typ                                          └────┘ 
doc                                           └────┘
137    (H : ∀ x : α, x ∈ s ↔ p x) :
id                       
src                       
typ                      
138    @card {x // p x} (fintype.subtype s H) = s.card :=
id      └──┘         └─────────────┘     └───┘
src     └──┘            └─────────────┘        └───┘
typ     └──┘         └─────────────┘     └───┘
doc     └──┘                                     └───┘
139  multiset.card_pmap _ _ _
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
140  
141  theorem card_of_subtype {p : α → Prop} (s : finset α)
id                                              └────┘ 
src                                              └────┘
typ                                             └────┘ 
doc                                              └────┘
142    (H : ∀ x : α, x ∈ s ↔ p x) [fintype {x // p x}] :
id                          └─────┘      
src                              └─────┘ 
typ                         └─────┘      
doc                                └─────┘
143    card {x // p x} = s.card :=
id     └──┘         └───┘
src    └──┘             └───┘
typ    └──┘         └───┘
doc    └──┘               └───┘
144  by rw ← subtype_card s H; congr
id           └──────────┘  
src     └───┘└──────────┘    └─────
typ     └───┘└──────────┘  └─────
doc     └───┘             
txt     └───┘                └─────
par     └───┘                └─────
pid       └─┘                     
st     └─────────────────────────────
145  
src  
typ  
txt  
par  
pid  
st   
146  /-- Construct a fintype from a finset with the same elements. -/
147  def of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : fintype p :=
id                      └─┘        └────┘                      └─────┘ 
src                     └─┘         └────┘                            └─────┘
typ                     └─┘        └────┘                      └─────┘ 
doc                                 └────┘                               └─────┘
148  fintype.subtype s H
id   └─────────────┘  
src  └─────────────┘
typ  └─────────────┘  
149  
150  @[simp] theorem card_of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) :
id                                       └─┘        └────┘                  
src                                      └─┘         └────┘                      
typ                                      └─┘        └────┘                  
doc    └──┘                                          └────┘
151    @fintype.card p (of_finset s H) = s.card :=
id      └──────────┘   └───────┘     └───┘
src     └──────────┘    └───────┘        └───┘
typ     └──────────┘   └───────┘     └───┘
doc     └──────────┘    └───────┘         └───┘
152  fintype.subtype_card s H
id   └──────────────────┘  
src  └──────────────────┘
typ  └──────────────────┘  
153  
154  theorem card_of_finset' {p : set α} (s : finset α)
id                                └─┘        └────┘ 
src                               └─┘         └────┘
typ                               └─┘        └────┘ 
doc                                           └────┘
155    (H : ∀ x, x ∈ s ↔ x ∈ p) [fintype p] : fintype.card p = s.card :=
id                       └─────┘     └──────────┘   └───┘
src                           └─────┘      └──────────┘     └───┘
typ                      └─────┘     └──────────┘   └───┘
doc                              └─────┘      └──────────┘      └───┘
156  by rw ← card_of_finset s H; congr
id           └────────────┘  
src     └───┘└────────────┘    └─────
typ     └───┘└────────────┘  └─────
doc     └───┘               
txt     └───┘                  └─────
par     └───┘                  └─────
pid       └─┘                       
st     └───────────────────────────────
157  
src  
typ  
txt  
par  
pid  
st   
158  /-- If `f : α → β` is a bijection and `α` is a fintype, then `β` is also a fintype. -/
159  def of_bijective [fintype α] (f : α → β) (H : function.bijective f) : fintype β :=
id                     └─────┘                  └────────────────┘     └─────┘ 
src                    └─────┘                     └────────────────┘      └─────┘
typ                    └─────┘                  └────────────────┘     └─────┘ 
doc                    └─────┘                                             └─────┘
160  ⟨univ.map ⟨f, H.1⟩,
id    └──┘└──┘    
src   └──┘└──┘      
typ   └──┘└──┘    
doc   └──┘
161  λ b, let ⟨a, e⟩ := H.2 b in e ▸ mem_map_of_mem _ (mem_univ _)⟩
id       └─┘                   └────────────┘    └──────┘
src                                └────────────┘    └──────┘
typ      └─┘                   └────────────┘    └──────┘
162  
163  /-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype. -/
164  def of_surjective [fintype α] [decidable_eq β] (f : α → β) (H : function.surjective f) : fintype β :=
id                      └─────┘    └──────────┘                  └─────────────────┘     └─────┘ 
src                     └─────┘     └──────────┘                     └─────────────────┘      └─────┘
typ                     └─────┘    └──────────┘                  └─────────────────┘     └─────┘ 
doc                     └─────┘                                                               └─────┘
165  ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
id    └──┘└────┘       └─┘                  └──────────────┘    └──────┘
src   └──┘└────┘                                 └──────────────┘    └──────┘
typ   └──┘└────┘       └─┘                  └──────────────┘    └──────┘
doc   └──┘└────┘
166  
167  noncomputable def of_injective [fintype β] (f : α → β) (H : function.injective f) : fintype α :=
id                                   └─────┘                  └────────────────┘     └─────┘ 
src                                  └─────┘                     └────────────────┘      └─────┘
typ                                  └─────┘                  └────────────────┘     └─────┘ 
doc                                  └─────┘                                             └─────┘
168  by letI := classical.dec; exact
id              └───────────┘
src     └──────┘└───────────┘  └────┘
typ     └──────┘└───────────┘  └────┘
doc     └──────┘               └────┘
txt     └──────┘               └────┘
par     └──────┘               └────┘
pid         └─┘                    
st     └─────────────────────────────
169  if hα : nonempty α then by letI := classical.inhabited_of_nonempty hα;
id   └┘      └──────┘                  └─────────────────────────────┘ └┘
src  └┘└────┘└──────┘ └────┘  └──────┘└─────────────────────────────┘  └─
typ  └┘└────┘└──────┘└────┘  └──────┘└─────────────────────────────┘└┘└─
doc    └────┘         └────┘  └──────┘                                 └─
txt    └────┘         └────┘  └──────┘                                 └─
par    └────┘         └────┘  └──────┘                                 └─
pid    └────┘         └────┘  └───────┘                                 └─
st   ─────────────────────────┘└────────────────────────────────────────────
170    exact of_surjective (inv_fun f) (inv_fun_surjective H)
id           └───────────┘  └─────┘    └────────────────┘ 
src  ───────┘└───────────┘ └─────┘ └┘ └────────────────┘ └─
typ  ───────┘└───────────┘ └─────┘└┘ └────────────────┘└─
doc  ───────┘└───────────┘ └─────┘ └┘                    └─
txt  ───────┘                      └┘                    └─
par  ───────┘                      └┘                    └─
pid  ───────┘                      └┘                    └─
st   ────────────────────────────────────────────────────────┘
171  else ⟨∅, λ x, (hα ⟨x⟩).elim⟩
id        
src  ────┘└┘ └──┘     └────────
typ  ────┘└┘ └──┘     └────────
doc  ────┘  └┘ └──┘     └────────
txt  ────┘  └┘ └──┘     └────────
par  ────┘  └┘ └──┘     └────────
pid  ────┘  └┘ └──┘     └──────┘
st   └────────────────────────────
172  
src  
typ  
doc  
txt  
par  
pid  
st   
173  /-- If `f : α ≃ β` and `α` is a fintype, then `β` is also a fintype. -/
174  def of_equiv (α : Type*) [fintype α] (f : α ≃ β) : fintype β := of_bijective _ f.bijective
id                             └─────┘              └─────┘     └──────────┘   └────────┘
src                            └─────┘                 └─────┘      └──────────┘    └────────┘
typ                            └─────┘              └─────┘     └──────────┘   └────────┘
doc                            └─────┘                 └─────┘      └──────────┘
175  
176  theorem of_equiv_card [fintype α] (f : α ≃ β) :
id                          └─────┘          
src                         └─────┘           
typ                         └─────┘          
doc                         └─────┘           
177    @card β (of_equiv α f) = card α :=
id      └──┘   └──────┘     └──┘ 
src     └──┘    └──────┘       └──┘
typ     └──┘   └──────┘     └──┘ 
doc     └──┘    └──────┘        └──┘
178  multiset.card_map _ _
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
179  
180  theorem card_congr {α β} [fintype α] [fintype β] (f : α ≃ β) : card α = card β :=
id                             └─────┘    └─────┘              └──┘   └──┘ 
src                            └─────┘     └─────┘                 └──┘    └──┘
typ                            └─────┘    └─────┘              └──┘   └──┘ 
doc                            └─────┘     └─────┘                 └──┘     └──┘
181  by rw ← of_equiv_card f; congr
id           └───────────┘ 
src     └───┘└───────────┘   └─────
typ     └───┘└───────────┘  └─────
doc     └───┘             
txt     └───┘                └─────
par     └───┘                └─────
pid       └─┘                     
st     └────────────────────────────
182  
src  
typ  
txt  
par  
pid  
st   
183  theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β ↔ nonempty (α ≃ β) :=
id                              └─────┘        └─────┘     └──┘   └──┘   └──────┘    
src                             └─────┘         └─────┘      └──┘    └──┘    └──────┘    
typ                             └─────┘        └─────┘     └──┘   └──┘   └──────┘    
doc                             └─────┘         └─────┘      └──┘     └──┘                 
184  ⟨λ h, ⟨by classical;
id      
src            └───────┘
typ           └───────┘
doc            └───────┘
txt            └───────┘
par            └───────┘
st            └───────────
185    calc α ≃ fin (card α) : trunc.out (equiv_fin α)
id     └──┘     └─┘  └──┘                           
src    └──┘     └─┘  └──┘
typ    └──┘     └─┘  └──┘                           
doc    └──┘          └──┘
st   ──────────────────────────────────────────────────
186       ... ≃ fin (card β) : by rw h
id                                   
src                               └─┘ 
typ                               └─┘
doc                               └─┘ 
txt                               └─┘ 
par                               └─┘ 
pid                                  
st   ───────────────────────────┘└─────
187       ... ≃ β : (trunc.out (equiv_fin β)).symm⟩,
id                   └───────┘  └───────┘   └──┘
src  ────┘           └───────┘  └───────┘    └──┘
typ  ────┘           └───────┘  └───────┘   └──┘
doc  ────┘           └───────┘  └───────┘
txt  ────┘
par  ────┘
pid  ────┘
st   ────┘└─────────────────────────────────────┘
188  λ ⟨f⟩, card_congr f⟩
id        └────────┘
src         └────────┘
typ       └────────┘
189  
190  def of_subsingleton (a : α) [subsingleton α] : fintype α :=
id                               └──────────┘     └─────┘ 
src                               └──────────┘      └─────┘
typ                              └──────────┘     └─────┘ 
doc                                                 └─────┘
191  ⟨finset.singleton a, λ b, finset.mem_singleton.2 (subsingleton.elim _ _)⟩
id    └──────────────┘       └──────────────────┘   └───────────────┘
src   └──────────────┘         └──────────────────┘   └───────────────┘
typ   └──────────────┘       └──────────────────┘   └───────────────┘
doc   └──────────────┘
192  
193  @[simp] theorem univ_of_subsingleton (a : α) [subsingleton α] :
id                                                └──────────┘ 
src                                                └──────────┘
typ                                               └──────────┘ 
doc    └──┘
194    @univ _ (of_subsingleton a) = finset.singleton a := rfl
id      └──┘    └─────────────┘    └──────────────┘     └─┘
src     └──┘    └─────────────┘     └──────────────┘      └─┘
typ     └──┘    └─────────────┘    └──────────────┘     └─┘
doc     └──┘                         └──────────────┘
195  
196  @[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
id                                                └──────────┘ 
src                                                └──────────┘
typ                                               └──────────┘ 
doc    └──┘
197    @fintype.card _ (of_subsingleton a) = 1 := rfl
id      └──────────┘    └─────────────┘         └─┘
src     └──────────┘    └─────────────┘          └─┘
typ     └──────────┘    └─────────────┘         └─┘
doc     └──────────┘
198  
199  lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
id                               └─────┘     └──────────┘    └─────────┘   └────┘  └─┘     
src                              └─────┘      └──────────┘     └─────────┘   └────┘   └─┘
typ                              └─────┘     └──────────┘    └─────────┘   └────┘  └─┘     
doc                              └─────┘      └──────────┘      └─────────┘   └────┘
200  finset.card_eq_sum_ones _
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
201  
202  end fintype
203  
204  namespace set
205  
206  /-- Construct a finset enumerating a set `s`, given a `fintype` instance.  -/
207  def to_finset (s : set α) [fintype s] : finset α :=
id                      └─┘    └─────┘     └────┘ 
src                     └─┘     └─────┘      └────┘
typ                     └─┘    └─────┘     └────┘ 
doc                             └─────┘      └────┘
208  ⟨(@finset.univ s _).1.map subtype.val,
id      └─────────┘     └─┘  └─────────┘
src     └─────────┘      └─┘  └─────────┘
typ     └─────────┘     └─┘  └─────────┘
doc     └─────────┘       └─┘
209   multiset.nodup_map (λ a b, subtype.eq) finset.univ.2⟩
id    └────────────────┘       └────────┘  └─────────┘
src   └────────────────┘         └────────┘  └─────────┘
typ   └────────────────┘       └────────┘  └─────────┘
doc                                          └─────────┘
210  
211  @[simp] theorem mem_to_finset {s : set α} [fintype s] {a : α} : a ∈ s.to_finset ↔ a ∈ s :=
id                                      └─┘    └─────┘              └────────┘    
src                                     └─┘     └─────┘                  └────────┘    
typ                                     └─┘    └─────┘              └────────┘    
doc    └──┘                                     └─────┘                   └────────┘
212  by simp [to_finset]
id            └───────┘
src     └────┘└───────┘└─
typ     └────┘└───────┘└─
doc     └────┘└───────┘└─
txt     └────┘         └─
par     └────┘         └─
pid                  
st     └─────────────────
213  
src  
typ  
doc  
txt  
par  
pid  
st   
214  @[simp] theorem mem_to_finset_val {s : set α} [fintype s] {a : α} : a ∈ s.to_finset.1 ↔ a ∈ s :=
id                                          └─┘    └─────┘              └────────┘     
src                                         └─┘     └─────┘                  └────────┘     
typ                                         └─┘    └─────┘              └────────┘     
doc    └──┘                                         └─────┘                   └────────┘
215  mem_to_finset
id   └───────────┘
src  └───────────┘
typ  └───────────┘
216  
217  end set
218  
219  lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
id                           └─────┘      └─────────┘   └────┘  └──┘   └──────────┘ 
src                          └─────┘       └─────────┘   └────┘   └──┘   └──────────┘
typ                          └─────┘      └─────────┘   └────┘  └──┘   └──────────┘ 
doc                          └─────┘       └─────────┘   └────┘   └──┘    └──────────┘
220  rfl
id   └─┘
src  └─┘
typ  └─┘
221  
222  lemma finset.card_univ_diff [fintype α] [decidable_eq α] (s : finset α) :
id                                └─────┘    └──────────┘        └────┘ 
src                               └─────┘     └──────────┘         └────┘
typ                               └─────┘    └──────────┘        └────┘ 
doc                               └─────┘                          └────┘
223    (finset.univ \ s).card = fintype.card α - s.card :=
id      └─────────┘   └──┘   └──────────┘   └───┘
src     └─────────┘    └──┘   └──────────┘     └───┘
typ     └─────────┘   └──┘   └──────────┘   └───┘
doc     └─────────┘     └──┘    └──────────┘      └───┘
224  finset.card_sdiff (subset_univ s)
id   └───────────────┘  └─────────┘ 
src  └───────────────┘  └─────────┘
typ  └───────────────┘  └─────────┘ 
225  
226  instance (n : ℕ) : fintype (fin n) :=
id                     └─────┘  └─┘ 
src                    └─────┘  └─┘
typ                    └─────┘  └─┘ 
doc                     └─────┘
227  ⟨⟨list.fin_range n, list.nodup_fin_range n⟩, list.mem_fin_range⟩
id     └────────────┘   └──────────────────┘    └────────────────┘
src    └────────────┘    └──────────────────┘     └────────────────┘
typ    └────────────┘   └──────────────────┘    └────────────────┘
doc    └────────────┘
228  
229  @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
id                                             └──────────┘  └─┘    
src                                            └──────────┘  └─┘    
typ                                            └──────────┘  └─┘    
doc    └──┘                                     └──────────┘
230  list.length_fin_range n
id   └───────────────────┘ 
src  └───────────────────┘
typ  └───────────────────┘ 
231  
232  lemma fin.univ_succ (n : ℕ) :
id                            
src                           
typ                           
233    (univ : finset (fin $ n+1)) = insert 0 (univ.image fin.succ) :=
id      └──┘   └────┘  └─┘        └────┘    └──┘└────┘ └──────┘
src     └──┘   └────┘  └─┘         └────┘    └──┘└────┘ └──────┘
typ     └──┘   └────┘  └─┘        └────┘    └──┘└────┘ └──────┘
doc     └──┘   └────┘                          └──┘└────┘
234  begin
st   └─────
235    ext m,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
236    simp only [mem_univ, mem_insert, true_iff, mem_image, exists_prop],
id                └──────┘  └────────┘  └──────┘  └───────┘  └─────────┘
src    └─────────┘└──────┘└┘└────────┘└┘└──────┘└┘└───────┘└┘└─────────┘
typ    └─────────┘└──────┘└┘└────────┘└┘└──────┘└┘└───────┘└┘└─────────┘
doc    └─────────┘        └┘          └┘        └┘         └┘           
txt    └─────────┘        └┘          └┘        └┘         └┘           
par    └─────────┘        └┘          └┘        └┘         └┘           
pid        └──┘└┘        └┘          └┘        └┘         └┘           
st   ───────────────────────────────────────────────────────────────────┘└─
237    exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m
id           └───────┘  └────┘            └────┘     └─────┘  └─┘   
src    └────┘└───────┘ └────┘   └┘  └──┘└────┘  └┘└─────┘└┘└─┘└─┘ 
typ    └────┘└───────┘ └────┘   └┘  └──┘└────┘  └┘└─────┘└┘└─┘└─┘
doc    └────┘                   └┘  └──┘        └┘       └┘   └─┘ 
txt    └────┘                   └┘  └──┘        └┘       └┘   └─┘ 
par    └────┘                   └┘  └──┘        └┘       └┘   └─┘ 
pid                            └┘  └──┘        └┘       └┘   └─┘ 
st   ────────────────────────────────────────────────────────────────┘
238  end
st   └─┘
239  
240  theorem fin.prod_univ_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
id                               └─────────┘             └─┘ └───┘   
src                              └─────────┘              └─┘  └───┘
typ                              └─────────┘             └─┘ └───┘   
241    univ.prod f = f 0 * univ.prod (λ i:fin n, f i.succ) :=
id     └──┘└───┘       └──┘└───┘      └─┘    └───┘
src    └──┘└───┘         └──┘└───┘      └─┘       └───┘
typ    └──┘└───┘       └──┘└───┘      └─┘    └───┘
doc    └──┘└───┘           └──┘└───┘
242  begin
st   └─────
243    rw [fin.univ_succ, prod_insert, prod_image],
id         └───────────┘  └─────────┘  └────────┘
src    └──┘└───────────┘└┘└─────────┘└┘└────────┘
typ    └──┘└───────────┘└┘└─────────┘└┘└────────┘
doc    └──┘             └┘           └┘          
txt    └──┘             └┘           └┘          
par    └──┘             └┘           └┘          
pid      └┘             └┘           └┘          
st   ──────────────────┘└───────────┘└──────────┘└──
244    { intros x _ y _ hxy, exact fin.succ.inj hxy },
id                                 └──────────┘ └─┘
src      └────────────────┘  └────┘└──────────┘   
typ      └────────────────┘  └────┘└──────────┘└─┘
doc      └────────────────┘  └────┘               
txt      └────────────────┘  └────┘               
par      └────────────────┘  └────┘               
pid            └──────────┘                      
st   ───┘└────────────────┘└───────────────────────┘└┘
245    { simpa using fin.succ_ne_zero }
id                   └──────────────┘
src      └──────────┘└──────────────┘
typ      └──────────┘└──────────────┘
doc      └──────────┘                
txt      └──────────┘                
par      └──────────┘                
pid           └────┘                
st   ────────────────────────────────┘└─
246  end
st   ──┘
247  
248  @[simp, to_additive] theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : univ.prod f = 1 := rfl
id                                                    └─────────┘        └─┘         └──┘└───┘        └─┘
src                                                   └─────────┘         └─┘          └──┘└───┘         └─┘
typ                                                   └─────────┘        └─┘         └──┘└───┘        └─┘
doc    └──┘  └─────────┘                                                               └──┘└───┘
249  
250  theorem fin.sum_univ_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
id                              └─────────────┘             └─┘ └───┘   
src                             └─────────────┘              └─┘  └───┘
typ                             └─────────────┘             └─┘ └───┘   
251    univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
id     └──┘└──┘       └──┘└──┘      └─┘    └───┘
src    └──┘└──┘         └──┘└──┘      └─┘       └───┘
typ    └──┘└──┘       └──┘└──┘      └─┘    └───┘
doc    └──┘               └──┘
252  by apply @fin.prod_univ_succ (multiplicative β)
id             └────────────────┘  └────────────┘ 
src     └────┘ └────────────────┘ └────────────┘ └─
typ     └────┘ └────────────────┘ └────────────┘└─
doc     └────┘                                   └─
txt     └────┘                                   └─
par     └────┘                                   └─
pid                                             
st     └─────────────────────────────────────────────
253  
src  
typ  
doc  
txt  
par  
pid  
st   
254  attribute [to_additive] fin.prod_univ_succ
id                           └────────────────┘
src                          └────────────────┘
typ                          └────────────────┘
doc             └─────────┘
255  
256  @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
id                                                            └────┘     └─────┘ 
src                                                           └────┘      └─────┘
typ                                                           └────┘     └─────┘ 
doc                                                                       └─────┘
257  ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
id    └──────────────┘  └─────┘               └───────────────┘ 
src   └──────────────┘  └─────┘             └──┘└───────────────┘   └──┘
typ   └──────────────┘  └─────┘           └──┘└───────────────┘  └──┘
doc   └──────────────┘                      └──┘                    └──┘
txt                                         └──┘                    └──┘
par                                         └──┘                    └──┘
pid                                           └┘                  
st                                         └──────────────────────┘└────┘
258  
259  @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
id                                          └────┘        └─────┘      └─────────┘     └─────┘ 
src                                         └────┘         └─────┘       └─────────┘      └─────┘
typ                                         └────┘        └─────┘      └─────────┘     └─────┘ 
doc    └──┘                                                └─────┘       └─────────┘
260  by rw [subsingleton.elim f (@unique.fintype α _)]; refl
id          └───────────────┘    └────────────┘ 
src     └──┘└───────────────┘   └────────────┘ └──┘  └────
typ     └──┘└───────────────┘  └────────────┘└──┘  └────
doc     └──┘                                   └──┘  └────
txt     └──┘                                   └──┘  └────
par     └──┘                                   └──┘  └────
pid       └┘                                   └──┘      
st     └────────────────────────────────────────────┘└──────
261  
src  
typ  
doc  
txt  
par  
pid  
st   
262  instance : fintype empty := ⟨∅, empty.rec _⟩
id              └─────┘ └───┘       └───────┘
src             └─────┘ └───┘       └───────┘
typ             └─────┘ └───┘       └───────┘
doc             └─────┘
263  
264  @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
id                                         └──┘ └───┘        └─┘
src                                        └──┘ └───┘        └─┘
typ                                        └──┘ └───┘        └─┘
doc    └──┘                                └──┘
265  
266  @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
id                                        └──────────┘ └───┘       └─┘
src                                       └──────────┘ └───┘       └─┘
typ                                       └──────────┘ └───┘       └─┘
doc    └──┘                               └──────────┘
267  
268  instance : fintype pempty := ⟨∅, pempty.rec _⟩
id              └─────┘ └────┘       └────────┘
src             └─────┘ └────┘       └────────┘
typ             └─────┘ └────┘       └────────┘
doc             └─────┘ └────┘
269  
270  @[simp] theorem fintype.univ_pempty : @univ pempty _ = ∅ := rfl
id                                          └──┘ └────┘        └─┘
src                                         └──┘ └────┘        └─┘
typ                                         └──┘ └────┘        └─┘
doc    └──┘                                 └──┘ └────┘
271  
272  @[simp] theorem fintype.card_pempty : fintype.card pempty = 0 := rfl
id                                         └──────────┘ └────┘       └─┘
src                                        └──────────┘ └────┘       └─┘
typ                                        └──────────┘ └────┘       └─┘
doc    └──┘                                └──────────┘ └────┘
273  
274  instance : fintype unit := fintype.of_subsingleton ()
id              └─────┘ └──┘    └─────────────────────┘ └┘
src             └─────┘ └──┘    └─────────────────────┘ └┘
typ             └─────┘ └──┘    └─────────────────────┘ └┘
doc             └─────┘ └──┘
275  
276  @[simp] theorem fintype.univ_unit : @univ unit _ = {()} := rfl
id                                        └──┘ └──┘    └┘     └─┘
src                                       └──┘ └──┘    └┘     └─┘
typ                                       └──┘ └──┘    └┘     └─┘
doc    └──┘                               └──┘ └──┘
277  
278  @[simp] theorem fintype.card_unit : fintype.card unit = 1 := rfl
id                                       └──────────┘ └──┘       └─┘
src                                      └──────────┘ └──┘       └─┘
typ                                      └──────────┘ └──┘       └─┘
doc    └──┘                              └──────────┘ └──┘
279  
280  instance : fintype punit := fintype.of_subsingleton punit.star
id              └─────┘ └───┘    └─────────────────────┘ └────────┘
src             └─────┘ └───┘    └─────────────────────┘ └────────┘
typ             └─────┘ └───┘    └─────────────────────┘ └────────┘
doc             └─────┘
281  
282  @[simp] theorem fintype.univ_punit : @univ punit _ = {punit.star} := rfl
id                                         └──┘ └───┘    └────────┘     └─┘
src                                        └──┘ └───┘    └────────┘     └─┘
typ                                        └──┘ └───┘    └────────┘     └─┘
doc    └──┘                                └──┘
283  
284  @[simp] theorem fintype.card_punit : fintype.card punit = 1 := rfl
id                                        └──────────┘ └───┘       └─┘
src                                       └──────────┘ └───┘       └─┘
typ                                       └──────────┘ └───┘       └─┘
doc    └──┘                               └──────────┘
285  
286  instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp⟩
id              └─────┘ └──┘      └┘└┘└┘└┘                          
src             └─────┘ └──┘      └┘└┘└┘└┘      └──┘           └────┘   └──┘
typ             └─────┘ └──┘      └┘└┘└┘└┘      └──┘          └────┘  └──┘
doc             └─────┘             └┘  └┘      └──┘           └────┘   └──┘
txt                                             └──┘           └────┘   └──┘
par                                             └──┘           └────┘   └──┘
pid                                                                 
st                                             └───┘          └────────────┘
287  
288  @[simp] theorem fintype.univ_bool : @univ bool _ = {ff, tt} := rfl
id                                        └──┘ └──┘    └┘ └┘     └─┘
src                                       └──┘ └──┘    └┘ └┘     └─┘
typ                                       └──┘ └──┘    └┘ └┘     └─┘
doc    └──┘                               └──┘
289  
290  instance units_int.fintype : fintype (units ℤ) :=
id                                └─────┘  └───┘ 
src                               └─────┘  └───┘ 
typ                               └─────┘  └───┘ 
doc                               └─────┘
291  ⟨{1, -1}, λ x, by cases int.units_eq_one_or x; simp *⟩
id                       └─────────────────┘ 
src                 └────┘└─────────────────┘   └────┘
typ                └────┘└─────────────────┘  └────┘
doc                    └────┘                      └────┘
txt                    └────┘                      └────┘
par                    └────┘                      └────┘
pid                                                   
st                    └──────────────────────────────────┘
292  
293  instance additive.fintype : Π [fintype α], fintype (additive α) := id
id                                  └─────┘    └─────┘  └──────┘      └┘
src                                 └─────┘     └─────┘  └──────┘       └┘
typ                                 └─────┘    └─────┘  └──────┘      └┘
doc                                 └─────┘     └─────┘
294  
295  instance multiplicative.fintype : Π [fintype α], fintype (multiplicative α) := id
id                                        └─────┘    └─────┘  └────────────┘      └┘
src                                       └─────┘     └─────┘  └────────────┘       └┘
typ                                       └─────┘    └─────┘  └────────────┘      └┘
doc                                       └─────┘     └─────┘
296  
297  @[simp] theorem fintype.card_units_int : fintype.card (units ℤ) = 2 := rfl
id                                            └──────────┘  └───┘         └─┘
src                                           └──────────┘  └───┘         └─┘
typ                                           └──────────┘  └───┘         └─┘
doc    └──┘                                   └──────────┘
298  
299  @[simp] theorem fintype.card_bool : fintype.card bool = 2 := rfl
id                                       └──────────┘ └──┘       └─┘
src                                      └──────────┘ └──┘       └─┘
typ                                      └──────────┘ └──┘       └─┘
doc    └──┘                              └──────────┘
300  
301  def finset.insert_none (s : finset α) : finset (option α) :=
id                               └────┘     └────┘  └────┘ 
src                              └────┘      └────┘  └────┘
typ                              └────┘     └────┘  └────┘ 
doc                              └────┘      └────┘
302  ⟨none :: s.1.map some, multiset.nodup_cons.2
id    └──┘ └┘  └─┘  └──┘  └─────────────────┘
src   └──┘ └┘   └─┘  └──┘  └─────────────────┘
typ   └──┘ └┘  └─┘  └──┘  └─────────────────┘
doc        └┘    └─┘
303    ⟨by simp, multiset.nodup_map (λ a b, option.some.inj) s.2⟩⟩
id               └────────────────┘       └─────────────┘  
src        └──┘  └────────────────┘         └─────────────┘   
typ        └──┘  └────────────────┘       └─────────────┘  
doc        └──┘
txt        └──┘
par        └──┘
st        └───┘
304  
305  @[simp] theorem finset.mem_insert_none {s : finset α} : ∀ {o : option α},
id                                               └────┘           └────┘ 
src                                              └────┘             └────┘
typ                                              └────┘           └────┘ 
doc    └──┘                                      └────┘
306    o ∈ s.insert_none ↔ ∀ a ∈ o, a ∈ s
id       └──────────┘           
src        └──────────┘             
typ      └──────────┘           
307  | none     := iff_of_true (multiset.mem_cons_self _ _) (λ a h, by cases h)
id     └──┘        └─────────┘  └────────────────────┘                     
src    └──┘        └─────────┘  └────────────────────┘                 └────┘
typ    └──┘        └─────────┘  └────────────────────┘               └────┘
doc                                                                    └────┘
txt                                                                    └────┘
par                                                                    └────┘
pid                                                                         
st                                                                    └──────┘
308  | (some a) := multiset.mem_cons.trans $ by simp; refl
id      └──┘       └───────────────┘└────┘
src     └──┘       └───────────────┘└────┘      └──┘  └────
typ     └──┘       └───────────────┘└────┘      └──┘  └────
doc                                             └──┘  └────
txt                                             └──┘  └────
par                                             └──┘  └────
pid                                                       
st                                             └───────────
309  
src  
typ  
doc  
txt  
par  
pid  
st   
310  theorem finset.some_mem_insert_none {s : finset α} {a : α} :
id                                            └────┘        
src                                           └────┘
typ                                           └────┘        
doc                                           └────┘
311    some a ∈ s.insert_none ↔ a ∈ s := by simp
id     └──┘   └──────────┘    
src    └──┘     └──────────┘             └────
typ    └──┘   └──────────┘           └────
doc                                         └────
txt                                         └────
par                                         └────
pid                                             
st                                         └─────
312  
src  
typ  
doc  
txt  
par  
pid  
st   
313  instance {α : Type*} [fintype α] : fintype (option α) :=
id                         └─────┘     └─────┘  └────┘ 
src                        └─────┘      └─────┘  └────┘
typ                        └─────┘     └─────┘  └────┘ 
doc                        └─────┘      └─────┘
314  ⟨univ.insert_none, λ a, by simp⟩
id    └──┘└──────────┘    
src   └──┘└──────────┘          └──┘
typ   └──┘└──────────┘         └──┘
doc   └──┘                      └──┘
txt                             └──┘
par                             └──┘
st                             └───┘
315  
316  @[simp] theorem fintype.card_option {α : Type*} [fintype α] :
id                                                    └─────┘ 
src                                                   └─────┘
typ                                                   └─────┘ 
doc    └──┘                                           └─────┘
317    fintype.card (option α) = fintype.card α + 1 :=
id     └──────────┘  └────┘    └──────────┘  
src    └──────────┘  └────┘     └──────────┘   
typ    └──────────┘  └────┘    └──────────┘  
doc    └──────────┘              └──────────┘
318  (multiset.card_cons _ _).trans (by rw multiset.card_map; refl)
id    └────────────────┘     └───┘         └───────────────┘
src   └────────────────┘     └───┘      └─┘└───────────────┘  └──┘
typ   └────────────────┘     └───┘      └─┘└───────────────┘  └──┘
doc                                     └─┘                   └──┘
txt                                     └─┘                   └──┘
par                                     └─┘                   └──┘
pid                                       
st                                     └─────────────────────────┘
319  
320  instance {α : Type*} (β : α → Type*)
id                             
typ                            
321    [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
id      └─────┘        └─────┘        └─────┘  └───┘ 
src     └─────┘          └─────┘          └─────┘  └───┘
typ     └─────┘        └─────┘        └─────┘  └───┘ 
doc     └─────┘          └─────┘          └─────┘
322  ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩
id    └──┘└────┘      └──┘     
src   └──┘└────┘       └──┘                └──┘
typ   └──┘└────┘      └──┘               └──┘
doc   └──┘└────┘       └──┘                └──┘
txt                                        └──┘
par                                        └──┘
st                                        └───┘
323  
324  @[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)
id                                                       
typ                                                      
doc    └──┘
325    [fintype α] [∀ a, fintype (β a)] :
id      └─────┘        └─────┘   
src     └─────┘          └─────┘
typ     └─────┘        └─────┘   
doc     └─────┘          └─────┘
326    fintype.card (sigma β) = univ.sum (λ a, fintype.card (β a)) :=
id     └──────────┘  └───┘    └──┘└──┘      └──────────┘   
src    └──────────┘  └───┘     └──┘└──┘       └──────────┘
typ    └──────────┘  └───┘    └──┘└──┘      └──────────┘   
doc    └──────────┘             └──┘           └──────────┘
327  card_sigma _ _
id   └────────┘
src  └────────┘
typ  └────────┘
328  
329  instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
id                           └─────┘    └─────┘     └─────┘    
src                          └─────┘     └─────┘      └─────┘    
typ                          └─────┘    └─────┘     └─────┘    
doc                          └─────┘     └─────┘      └─────┘
330  ⟨univ.product univ, λ ⟨a, b⟩, by simp⟩
id    └──┘└──────┘ └──┘    
src   └──┘└──────┘ └──┘               └──┘
typ   └──┘└──────┘ └──┘              └──┘
doc   └──┘└──────┘ └──┘               └──┘
txt                                   └──┘
par                                   └──┘
st                                   └───┘
331  
332  @[simp] theorem fintype.card_prod (α β : Type*) [fintype α] [fintype β] :
id                                                    └─────┘    └─────┘ 
src                                                   └─────┘     └─────┘
typ                                                   └─────┘    └─────┘ 
doc    └──┘                                           └─────┘     └─────┘
333    fintype.card (α × β) = fintype.card α * fintype.card β :=
id     └──────────┘       └──────────┘   └──────────┘ 
src    └──────────┘         └──────────┘    └──────────┘
typ    └──────────┘       └──────────┘   └──────────┘ 
doc    └──────────┘           └──────────┘     └──────────┘
334  card_product _ _
id   └──────────┘
src  └──────────┘
typ  └──────────┘
335  
336  def fintype.fintype_prod_left {α β} [decidable_eq α] [fintype (α × β)] [nonempty β] : fintype α :=
id                                        └──────────┘    └─────┘        └──────┘     └─────┘ 
src                                       └──────────┘     └─────┘          └──────┘      └─────┘
typ                                       └──────────┘    └─────┘        └──────┘     └─────┘ 
doc                                                        └─────┘                         └─────┘
337  ⟨(fintype.elems (α × β)).image prod.fst,
id     └───────────┘      └───┘  └──────┘
src    └───────────┘        └───┘  └──────┘
typ    └───────────┘      └───┘  └──────┘
doc                          └───┘
338    assume a, let ⟨b⟩ := ‹nonempty β› in by simp; exact ⟨b, fintype.complete _⟩⟩
id              └─┘        └──────┘                       └──────────────┘
src                         └──────┘         └──┘  └────┘  └┘└──────────────┘└─┘
typ             └─┘        └──────┘        └──┘  └────┘ └┘└──────────────┘└─┘
doc                                          └──┘  └────┘  └┘                └─┘
txt                                            └──┘  └────┘  └┘                └─┘
par                                            └──┘  └────┘  └┘                └─┘
pid                                                         └┘                └─┘
st                                            └──────────────────────────────────┘
339  
340  def fintype.fintype_prod_right {α β} [decidable_eq β] [fintype (α × β)] [nonempty α] : fintype β :=
id                                         └──────────┘    └─────┘        └──────┘     └─────┘ 
src                                        └──────────┘     └─────┘          └──────┘      └─────┘
typ                                        └──────────┘    └─────┘        └──────┘     └─────┘ 
doc                                                         └─────┘                         └─────┘
341  ⟨(fintype.elems (α × β)).image prod.snd,
id     └───────────┘      └───┘  └──────┘
src    └───────────┘        └───┘  └──────┘
typ    └───────────┘      └───┘  └──────┘
doc                          └───┘
342    assume b, let ⟨a⟩ := ‹nonempty α› in by simp; exact ⟨a, fintype.complete _⟩⟩
id              └─┘        └──────┘                       └──────────────┘
src                         └──────┘         └──┘  └────┘  └┘└──────────────┘└─┘
typ             └─┘        └──────┘        └──┘  └────┘ └┘└──────────────┘└─┘
doc                                          └──┘  └────┘  └┘                └─┘
txt                                            └──┘  └────┘  └┘                └─┘
par                                            └──┘  └────┘  └┘                └─┘
pid                                                         └┘                └─┘
st                                            └──────────────────────────────────┘
343  
344  instance (α : Type*) [fintype α] : fintype (ulift α) :=
id                         └─────┘     └─────┘  └───┘ 
src                        └─────┘      └─────┘  └───┘
typ                        └─────┘     └─────┘  └───┘ 
doc                        └─────┘      └─────┘  └───┘
345  fintype.of_equiv _ equiv.ulift.symm
id   └──────────────┘   └─────────┘└───┘
src  └──────────────┘   └─────────┘└───┘
typ  └──────────────┘   └─────────┘└───┘
doc  └──────────────┘
346  
347  @[simp] theorem fintype.card_ulift (α : Type*) [fintype α] :
id                                                   └─────┘ 
src                                                  └─────┘
typ                                                  └─────┘ 
doc    └──┘                                          └─────┘
348    fintype.card (ulift α) = fintype.card α :=
id     └──────────┘  └───┘    └──────────┘ 
src    └──────────┘  └───┘     └──────────┘
typ    └──────────┘  └───┘    └──────────┘ 
doc    └──────────┘  └───┘      └──────────┘
349  fintype.of_equiv_card _
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
350  
351  instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕ β) :=
id                                       └─────┘    └─────┘     └─────┘    
src                                      └─────┘     └─────┘      └─────┘    
typ                                      └─────┘    └─────┘     └─────┘    
doc                                      └─────┘     └─────┘      └─────┘
352  @fintype.of_equiv _ _ (@sigma.fintype _
id    └──────────────┘       └───────────┘
src   └──────────────┘       └───────────┘
typ   └──────────────┘       └───────────┘
doc   └──────────────┘
353      (λ b, cond b (ulift α) (ulift.{(max u v) v} β)) _
id            └──┘   └───┘    └───┘               
src            └──┘    └───┘     └───┘
typ           └──┘   └───┘    └───┘               
doc                    └───┘     └───┘
354      (λ b, by cases b; apply ulift.fintype))
id                             └───────────┘
src               └────┘   └────┘└───────────┘
typ              └────┘  └────┘└───────────┘
doc               └────┘   └────┘
txt               └────┘   └────┘
par               └────┘   └────┘
pid                            
st               └───────────────────────────┘
355    ((equiv.sum_equiv_sigma_bool _ _).symm.trans
id       └────────────────────────┘     └──┘ └───┘
src      └────────────────────────┘     └──┘ └───┘
typ      └────────────────────────┘     └──┘ └───┘
356      (equiv.sum_congr equiv.ulift equiv.ulift))
id        └─────────────┘ └─────────┘ └─────────┘
src       └─────────────┘ └─────────┘ └─────────┘
typ       └─────────────┘ └─────────┘ └─────────┘
357  
358  @[simp] theorem fintype.card_sum (α β : Type*) [fintype α] [fintype β] :
id                                                   └─────┘    └─────┘ 
src                                                  └─────┘     └─────┘
typ                                                  └─────┘    └─────┘ 
doc    └──┘                                          └─────┘     └─────┘
359    fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
id     └──────────┘       └──────────┘   └──────────┘ 
src    └──────────┘         └──────────┘    └──────────┘
typ    └──────────┘       └──────────┘   └──────────┘ 
doc    └──────────┘           └──────────┘     └──────────┘
360  by rw [sum.fintype, fintype.of_equiv_card]; simp
id          └─────────┘  └───────────────────┘
src     └──┘└─────────┘└┘└───────────────────┘  └────
typ     └──┘└─────────┘└┘└───────────────────┘  └────
doc     └──┘           └┘                       └────
txt     └──┘           └┘                       └────
par     └──┘           └┘                       └────
pid       └┘           └┘                           
st     └──────────────┘└─────────────────────┘└──────
361  
src  
typ  
doc  
txt  
par  
pid  
st   
362  lemma fintype.card_le_of_injective [fintype α] [fintype β] (f : α → β)
id                                       └─────┘    └─────┘           
src                                      └─────┘     └─────┘
typ                                      └─────┘    └─────┘           
doc                                      └─────┘     └─────┘
363    (hf : function.injective f) : fintype.card α ≤ fintype.card β :=
id           └────────────────┘     └──────────┘   └──────────┘ 
src          └────────────────┘      └──────────┘    └──────────┘
typ          └────────────────┘     └──────────┘   └──────────┘ 
doc                                  └──────────┘     └──────────┘
364  by haveI := classical.prop_decidable; exact
id               └──────────────────────┘
src     └───────┘└──────────────────────┘  └────┘
typ     └───────┘└──────────────────────┘  └────┘
doc     └───────┘                          └────┘
txt     └───────┘                          └────┘
par     └───────┘                          └────┘
pid          └─┘                               
st     └─────────────────────────────────────────
365  finset.card_le_card_of_inj_on f (λ _ _, finset.mem_univ _) (λ _ _ _ _ h, hf h)
id   └───────────────────────────┘          └─────────────┘                  └┘
src  └───────────────────────────┘   └────┘└─────────────┘└──┘  └──────────┘   └─
typ  └───────────────────────────┘  └────┘└─────────────┘└──┘  └──────────┘└┘ └─
doc                                  └────┘               └──┘  └──────────┘   └─
txt                                  └────┘               └──┘  └──────────┘   └─
par                                  └────┘               └──┘  └──────────┘   └─
pid                                  └────┘               └──┘  └──────────┘   
st   ───────────────────────────────────────────────────────────────────────────────
366  
src  
typ  
doc  
txt  
par  
pid  
st   
367  lemma fintype.card_eq_one_iff [fintype α] : fintype.card α = 1 ↔ (∃ x : α, ∀ y, y = x) :=
id                                  └─────┘     └──────────┘                   
src                                 └─────┘      └──────────┘                      
typ                                 └─────┘     └──────────┘                   
doc                                 └─────┘      └──────────┘
368  by rw [← fintype.card_unit, fintype.card_eq]; exact
id            └───────────────┘  └─────────────┘
src     └────┘└───────────────┘└┘└─────────────┘  └────┘
typ     └────┘└───────────────┘└┘└─────────────┘  └────┘
doc     └────┘                 └┘                 └────┘
txt     └────┘                 └┘                 └────┘
par     └────┘                 └┘                 └────┘
pid       └──┘                 └┘                      
st     └──────────────────────┘└───────────────┘└───────
369  ⟨λ ⟨a⟩, ⟨a.symm (), λ y, a.injective (subsingleton.elim _ _)⟩,
id            └───┘ └┘        └────────┘
src    └┘ └─┘  └───┘└┘└┘ └──┘ └────────┘                  └───────
typ    └┘└─┘  └───┘└┘└┘ └──┘ └────────┘                  └───────
doc    └┘ └─┘         └┘ └──┘                             └───────
txt    └┘ └─┘         └┘ └──┘                             └───────
par    └┘ └─┘         └┘ └──┘                             └───────
pid    └┘ └─┘         └┘ └──┘                             └───────
st   ───────────────────────────────────────────────────────────────
370    λ ⟨x, hx⟩, ⟨⟨λ _, (), λ _, x, λ _, (hx _).trans (hx _).symm,
id          └┘
src  ─┘ └┘ └┘  └─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
typ  ─┘ └┘└┘└┘└─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
doc  ─┘ └┘ └┘  └─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
txt  ─┘ └┘ └┘  └─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
par  ─┘ └┘ └┘  └─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
pid  ─┘ └┘ └┘  └─┘   └──┘  └┘ └──┘ └┘ └──┘   └────────┘   └─────────
st   ───────────────────────────────────────────────────────────────
371      λ _, subsingleton.elim _ _⟩⟩⟩
id            └───────────────┘
src  ───┘ └──┘└───────────────┘└───────
typ  ───┘ └──┘└───────────────┘└───────
doc  ───┘ └──┘                 └───────
txt  ───┘ └──┘                 └───────
par  ───┘ └──┘                 └───────
pid  ───┘ └──┘                 └─────┘
st   ──────────────────────────────────
372  
src  
typ  
doc  
txt  
par  
pid  
st   
373  lemma fintype.card_eq_zero_iff [fintype α] : fintype.card α = 0 ↔ (α → false) :=
id                                   └─────┘     └──────────┘          └───┘
src                                  └─────┘      └──────────┘            └───┘
typ                                  └─────┘     └──────────┘          └───┘
doc                                  └─────┘      └──────────┘
374  ⟨λ h a, have e : α ≃ empty := classical.choice (fintype.card_eq.1 (by simp [h])), (e a).elim,
id                    └───┘    └──────────────┘  └─────────────┘                    └──┘
src                      └───┘    └──────────────┘  └─────────────┘      └────┘          └──┘
typ                   └───┘    └──────────────┘  └─────────────┘      └────┘       └──┘
doc                                                                       └────┘ 
txt                                                                        └────┘ 
par                                                                        └────┘ 
pid                                                                             
st                                                                        └───────┘
375    λ h, have e : α ≃ empty := ⟨λ a, (h a).elim, λ a, a.elim, λ a, (h a).elim, λ a, a.elim⟩,
id                    └───┘            └──┘       └───┘         └──┘       └───┘
src                     └───┘               └──┘         └───┘            └──┘         └───┘
typ                   └───┘            └──┘       └───┘         └──┘       └───┘
doc                    
376      by simp [fintype.card_congr e]⟩
id                └────────────────┘ 
src         └────┘└────────────────┘ 
typ         └────┘└────────────────┘
doc         └────┘                   
txt         └────┘                   
par         └────┘                   
pid                                
st         └──────────────────────────┘
377  
378  lemma fintype.card_pos_iff [fintype α] : 0 < fintype.card α ↔ nonempty α :=
id                               └─────┘        └──────────┘   └──────┘ 
src                              └─────┘         └──────────┘    └──────┘
typ                              └─────┘        └──────────┘   └──────┘ 
doc                              └─────┘          └──────────┘
379  ⟨λ h, classical.by_contradiction (λ h₁,
id        └────────────────────────┘    └┘
src        └────────────────────────┘
typ       └────────────────────────┘    └┘
380    have fintype.card α = 0 := fintype.card_eq_zero_iff.2 (λ a, h₁ ⟨a⟩),
id          └──────────┘        └──────────────────────┘       └┘  
src         └──────────┘         └──────────────────────┘
typ         └──────────┘        └──────────────────────┘       └┘  
doc         └──────────┘
381    lt_irrefl 0 $ by rwa this at h),
id     └───────┘            └──┘
src    └───────┘        └──┘    └───┘
typ    └───────┘        └──┘└──┘└───┘
doc                     └──┘    └───┘
txt                     └──┘    └───┘
par                     └──┘    └───┘
pid                            └───┘
st                     └────────────┘
382  λ ⟨a⟩, nat.pos_of_ne_zero (mt fintype.card_eq_zero_iff.1 (λ h, h a))⟩
id        └────────────────┘  └┘ └──────────────────────┘       
src         └────────────────┘  └┘ └──────────────────────┘
typ       └────────────────┘  └┘ └──────────────────────┘       
383  
384  lemma fintype.card_le_one_iff [fintype α] : fintype.card α ≤ 1 ↔ (∀ a b : α, a = b) :=
id                                  └─────┘     └──────────┘                   
src                                 └─────┘      └──────────┘                     
typ                                 └─────┘     └──────────┘                   
doc                                 └─────┘      └──────────┘
385  let n := fintype.card α in
id           └──────────┘ 
src           └──────────┘
typ          └──────────┘ 
doc           └──────────┘
386  have hn : n = fintype.card α := rfl,
id               └──────────┘     └─┘
src               └──────────┘      └─┘
typ              └──────────┘     └─┘
doc                └──────────┘
387  match n, hn with
id           └┘
typ          └┘
388  | 0 := λ ha, ⟨λ h, λ a, (fintype.card_eq_zero_iff.1 ha.symm a).elim, λ _, ha ▸ nat.le_succ _⟩
id            └┘            └──────────────────────┘  └┘└───┘  └──┘       └┘  └─────────┘
src                           └──────────────────────┘    └───┘   └──┘            └─────────┘
typ           └┘            └──────────────────────┘  └┘└───┘  └──┘       └┘  └─────────┘
389  | 1 := λ ha, ⟨λ h, λ a b, let ⟨x, hx⟩ := fintype.card_eq_one_iff.1 ha.symm in
id            └┘            └─┘            └─────────────────────┘  └┘└───┘
src                                           └─────────────────────┘    └───┘
typ           └┘            └─┘            └─────────────────────┘  └┘└───┘
390    by rw [hx a, hx b],
id            └┘   └┘ 
src       └──┘   └┘   
typ       └──┘└┘└┘└┘
doc       └──┘   └┘   
txt       └──┘   └┘   
par       └──┘   └┘   
pid         └┘   └┘   
st       └───────┘└────┘
391      λ _, ha ▸ le_refl _⟩
id           └┘  └─────┘
src               └─────┘
typ          └┘  └─────┘
392  | (n+2) := λ ha, ⟨λ h, by rw ← ha at h; exact absurd h dec_trivial,
id               └┘               └┘             └────┘  └─────────┘
src                           └───┘  └───┘  └────┘└────┘ └─────────┘
typ              └┘          └───┘└┘└───┘  └────┘└────┘└─────────┘
doc                            └───┘  └───┘  └────┘       └─────────┘
txt                            └───┘  └───┘  └────┘       
par                            └───┘  └───┘  └────┘       
pid                              └─┘  └───┘              
st                            └───────────────────────────────────────┘
393    (λ h, fintype.card_unit ▸ fintype.card_le_of_injective (λ _, ())
id          └───────────────┘  └──────────────────────────┘      └┘
src          └───────────────┘  └──────────────────────────┘       └┘
typ         └───────────────┘  └──────────────────────────┘      └┘
394      (λ _ _ _, h _ _))⟩
id              
typ             
395  end
396  
397  lemma fintype.exists_ne_of_one_lt_card [fintype α] (h : 1 < fintype.card α) (a : α) :
id                                           └─────┘           └──────────┘        
src                                          └─────┘            └──────────┘
typ                                          └─────┘           └──────────┘        
doc                                          └─────┘             └──────────┘
398    ∃ b : α, b ≠ a :=
id             
src             
typ            
399  let ⟨b, hb⟩ := classical.not_forall.1 (mt fintype.card_le_one_iff.2 (not_le_of_gt h)) in
id   └─┘     └┘     └──────────────────┘   └┘ └─────────────────────┘   └──────────┘ 
src                 └──────────────────┘   └┘ └─────────────────────┘   └──────────┘
typ  └─┘     └┘     └──────────────────┘   └┘ └─────────────────────┘   └──────────┘ 
400  let ⟨c, hc⟩ := classical.not_forall.1 hb in
id   └─┘            └──────────────────┘
src                 └──────────────────┘
typ  └─┘            └──────────────────┘
401  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
402  if hba : b = a then ⟨c, by cc⟩ else ⟨b, hba⟩
id   └┘                               
src  └┘└─────┘  └────┘  └┘  └┘└─────┘  └┘   └─
typ  └┘└─────┘ └────┘ └┘  └┘└─────┘└┘   └─
doc    └─────┘   └────┘  └┘  └┘└─────┘  └┘   └─
txt    └─────┘   └────┘  └┘  └┘└─────┘  └┘   └─
par    └─────┘   └────┘  └┘  └┘└─────┘  └┘   └─
pid    └─────┘   └────┘  └┘  └────────┘  └┘   
st   ─────────────────────────┘└─┘└───────────────
403  
src  
typ  
doc  
txt  
par  
pid  
st   
404  lemma fintype.injective_iff_surjective [fintype α] {f : α → α} : injective f ↔ surjective f :=
id                                           └─────┘               └───────┘   └────────┘ 
src                                          └─────┘                  └───────┘    └────────┘
typ                                          └─────┘               └───────┘   └────────┘ 
doc                                          └─────┘
405  by haveI := classical.prop_decidable; exact
id               └──────────────────────┘
src     └───────┘└──────────────────────┘  └────┘
typ     └───────┘└──────────────────────┘  └────┘
doc     └───────┘                          └────┘
txt     └───────┘                          └────┘
par     └───────┘                          └────┘
pid          └─┘                               
st     └─────────────────────────────────────────
406  have ∀ {f : α → α}, injective f → surjective f,
id                     └───────┘     └────────┘
src       └────┘    └───────┘  └────────┘ └─
typ       └────┘  └───────┘  └────────┘ └─
doc       └────┘                          └─
txt       └────┘                          └─
par       └────┘                          └─
pid       └────┘                          └─
st   ────────────────────────────────────────────────
407  from λ f hinj x,
src  ────┘ └──────────
typ  ────┘ └──────────
doc  ────┘ └──────────
txt  ────┘ └──────────
par  ────┘ └──────────
pid  ────┘ └──────────
st   ─────────────────
408    have h₁ : image f univ = univ := eq_of_subset_of_card_le (subset_univ _)
id                                     └─────────────────────┘  └─────────┘
src  ─┘    └────┘              └──┘└─────────────────────┘ └─────────┘└───
typ  ─┘    └────┘              └──┘└─────────────────────┘ └─────────┘└───
doc  ─┘    └────┘               └──┘                                   └───
txt  ─┘    └────┘               └──┘                                   └───
par  ─┘    └────┘               └──┘                                   └───
pid  ─┘    └────┘               └──┘                                   └───
st   ───────────────────────────────────────────────────────────────────────────
409      ((card_image_of_injective univ hinj).symm ▸ le_refl _),
id         └─────────────────────┘ └──┘              └─────┘
src  ───┘  └─────────────────────┘└──┘    └─────┘ └─────┘└────
typ  ───┘  └─────────────────────┘└──┘    └─────┘ └─────┘└────
doc  ───┘                         └──┘    └─────┘        └────
txt  ───┘                                 └─────┘        └────
par  ───┘                                 └─────┘        └────
pid  ───┘                                 └─────┘        └────
st   ────────────────────────────────────────────────────────────
410    have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ _,
id                  └───┘             └───┘  └──────┘
src  ─┘    └────┘ └───┘     └──┘  └───┘└──────┘└───
typ  ─┘    └────┘ └───┘     └──┘  └───┘└──────┘└───
doc  ─┘    └────┘  └───┘     └──┘                └───
txt  ─┘    └────┘            └──┘                └───
par  ─┘    └────┘            └──┘                └───
pid  ─┘    └────┘            └──┘                └───
st   ──────────────────────────────────────────────────────
411    exists_of_bex (mem_image.1 h₂),
id     └───────────┘  └───────┘
src  ─┘└───────────┘ └───────┘└─┘  └─┘
typ  ─┘└───────────┘ └───────┘└─┘  └─┘
doc  ─┘                       └─┘  └─┘
txt  ─┘                       └─┘  └─┘
par  ─┘                       └─┘  └─┘
pid  ─┘                       └─┘  └─┘
st   ──────────────────────────────────
412  ⟨this,
src       └─
typ       └─
doc       └─
txt       └─
par       └─
pid       └─
st   ───────
413    λ hsurj, injective_of_has_left_inverse
id              └───────────────────────────┘
src  ─┘ └──────┘└───────────────────────────┘
typ  ─┘ └──────┘└───────────────────────────┘
doc  ─┘ └──────┘                             
txt  ─┘ └──────┘                             
par  ─┘ └──────┘                             
pid  ─┘ └──────┘                             
st   ─────────────────────────────────────────
414      ⟨surj_inv hsurj, left_inverse_of_surjective_of_right_inverse
id        └──────┘        └─────────────────────────────────────────┘
src  ───┘ └──────┘     └┘└─────────────────────────────────────────┘
typ  ───┘ └──────┘     └┘└─────────────────────────────────────────┘
doc  ───┘ └──────┘     └┘                                           
txt  ───┘              └┘                                           
par  ───┘              └┘                                           
pid  ───┘              └┘                                           
st   ─────────────────────────────────────────────────────────────────
415        (this (injective_surj_inv _)) (right_inverse_surj_inv _)⟩⟩
id                └────────────────┘      └────────────────────┘
src  ─────┘      └────────────────┘└───┘ └────────────────────┘└─────
typ  ─────┘      └────────────────┘└───┘ └────────────────────┘└─────
doc  ─────┘                        └───┘                       └─────
txt  ─────┘                        └───┘                       └─────
par  ─────┘                        └───┘                       └─────
pid  ─────┘                        └───┘                       └───┘
st   ─────────────────────────────────────────────────────────────────
416  
src  
typ  
doc  
txt  
par  
pid  
st   
417  lemma fintype.injective_iff_bijective [fintype α] {f : α → α} : injective f ↔ bijective f :=
id                                          └─────┘               └───────┘   └───────┘ 
src                                         └─────┘                  └───────┘    └───────┘
typ                                         └─────┘               └───────┘   └───────┘ 
doc                                         └─────┘
418  by simp [bijective, fintype.injective_iff_surjective]
id            └───────┘  └──────────────────────────────┘
src     └────┘└───────┘└┘└──────────────────────────────┘└─
typ     └────┘└───────┘└┘└──────────────────────────────┘└─
doc     └────┘         └┘                                └─
txt     └────┘         └┘                                └─
par     └────┘         └┘                                └─
pid                  └┘                                
st     └───────────────────────────────────────────────────
419  
src  
typ  
doc  
txt  
par  
pid  
st   
420  lemma fintype.surjective_iff_bijective [fintype α] {f : α → α} : surjective f ↔ bijective f :=
id                                           └─────┘               └────────┘   └───────┘ 
src                                          └─────┘                  └────────┘    └───────┘
typ                                          └─────┘               └────────┘   └───────┘ 
doc                                          └─────┘
421  by simp [bijective, fintype.injective_iff_surjective]
id            └───────┘  └──────────────────────────────┘
src     └────┘└───────┘└┘└──────────────────────────────┘└─
typ     └────┘└───────┘└┘└──────────────────────────────┘└─
doc     └────┘         └┘                                └─
txt     └────┘         └┘                                └─
par     └────┘         └┘                                └─
pid                  └┘                                
st     └───────────────────────────────────────────────────
422  
src  
typ  
doc  
txt  
par  
pid  
st   
423  lemma fintype.injective_iff_surjective_of_equiv [fintype α] {f : α → β} (e : α ≃ β) :
id                                                    └─────┘                    
src                                                   └─────┘                       
typ                                                   └─────┘                    
doc                                                   └─────┘                       
424    injective f ↔ surjective f :=
id     └───────┘   └────────┘ 
src    └───────┘    └────────┘
typ    └───────┘   └────────┘ 
425  have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from fintype.injective_iff_surjective,
id        └───────┘  └───┘     └────────┘  └───┘          └──────────────────────────────┘
src       └───────┘   └───┘      └────────┘   └───┘           └──────────────────────────────┘
typ       └───────┘  └───┘     └────────┘  └───┘          └──────────────────────────────┘
426  ⟨λ hinj, by simpa [function.comp] using
id      └──┘            └───────────┘
src              └─────┘└───────────┘└───────
typ     └──┘     └─────┘└───────────┘└───────
doc              └─────┘             └───────
txt              └─────┘             └───────
par              └─────┘             └───────
pid                                └─────
st              └────────────────────────────
427    surjective_comp e.surjective (this.1 (injective_comp e.symm.injective hinj)),
id     └─────────────┘ └──────────┘  └──┘    └────────────┘ └──────────────┘ └──┘
src  ─┘└─────────────┘└──────────┘     └─┘ └────────────┘└──────────────┘    └┘
typ  ─┘└─────────────┘└──────────┘ └──┘└─┘ └────────────┘└──────────────┘└──┘└┘
doc  ─┘                                └─┘                                   └┘
txt  ─┘                                └─┘                                   └┘
par  ─┘                                └─┘                                   └┘
pid  ─┘                                └─┘                                   └┘
st   ─────────────────────────────────────────────────────────────────────────────┘
428  λ hsurj, by simpa [function.comp] using
id     └───┘            └───────────┘
src              └─────┘└───────────┘└───────
typ    └───┘     └─────┘└───────────┘└───────
doc              └─────┘             └───────
txt              └─────┘             └───────
par              └─────┘             └───────
pid                                └─────
st              └────────────────────────────
429    injective_comp e.injective (this.2 (surjective_comp e.symm.surjective hsurj))⟩
id     └────────────┘ └─────────┘  └──┘    └─────────────┘ └───────────────┘ └───┘
src  ─┘└────────────┘└─────────┘     └─┘ └─────────────┘└───────────────┘     └┘
typ  ─┘└────────────┘└─────────┘ └──┘└─┘ └─────────────┘└───────────────┘└───┘└┘
doc  ─┘                              └─┘                                      └┘
txt  ─┘                              └─┘                                      └┘
par  ─┘                              └─┘                                      └┘
pid  ─┘                              └─┘                                      └┘
st   ──────────────────────────────────────────────────────────────────────────────┘
430  
431  instance list.subtype.fintype [decidable_eq α] (l : list α) : fintype {x // x ∈ l} :=
id                                  └──────────┘        └──┘     └─────┘       
src                                 └──────────┘         └──┘      └─────┘        
typ                                 └──────────┘        └──┘     └─────┘       
doc                                                                └─────┘
432  fintype.of_list l.attach l.mem_attach
id   └─────────────┘ └─────┘ └─────────┘
src  └─────────────┘  └─────┘  └─────────┘
typ  └─────────────┘ └─────┘ └─────────┘
doc  └─────────────┘  └─────┘
433  
434  instance multiset.subtype.fintype [decidable_eq α] (s : multiset α) : fintype {x // x ∈ s} :=
id                                      └──────────┘        └──────┘     └─────┘       
src                                     └──────────┘         └──────┘      └─────┘        
typ                                     └──────────┘        └──────┘     └─────┘       
doc                                                          └──────┘      └─────┘
435  fintype.of_multiset s.attach s.mem_attach
id   └─────────────────┘ └─────┘ └─────────┘
src  └─────────────────┘  └─────┘  └─────────┘
typ  └─────────────────┘ └─────┘ └─────────┘
doc  └─────────────────┘  └─────┘
436  
437  instance finset.subtype.fintype (s : finset α) : fintype {x // x ∈ s} :=
id                                        └────┘     └─────┘       
src                                       └────┘      └─────┘        
typ                                       └────┘     └─────┘       
doc                                       └────┘      └─────┘
438  ⟨s.attach, s.mem_attach⟩
id    └─────┘  └─────────┘
src    └─────┘   └─────────┘
typ   └─────┘  └─────────┘
doc    └─────┘
439  
440  instance finset_coe.fintype (s : finset α) : fintype (↑s : set α) :=
id                                    └────┘     └─────┘     └─┘ 
src                                   └────┘      └─────┘      └─┘
typ                                   └────┘     └─────┘     └─┘ 
doc                                   └────┘      └─────┘
441  finset.subtype.fintype s
id   └────────────────────┘ 
src  └────────────────────┘
typ  └────────────────────┘ 
442  
443  @[simp] lemma fintype.card_coe (s : finset α) :
id                                       └────┘ 
src                                      └────┘
typ                                      └────┘ 
doc    └──┘                              └────┘
444    fintype.card (↑s : set α) = s.card := card_attach
id     └──────────┘     └─┘    └───┘    └─────────┘
src    └──────────┘      └─┘      └───┘    └─────────┘
typ    └──────────┘     └─┘    └───┘    └─────────┘
doc    └──────────┘                 └───┘
445  
446  instance plift.fintype (p : Prop) [decidable p] : fintype (plift p) :=
id                                      └───────┘     └─────┘  └───┘ 
src                                     └───────┘      └─────┘  └───┘
typ                                     └───────┘     └─────┘  └───┘ 
doc                                                    └─────┘  └───┘
447  ⟨if h : p then finset.singleton ⟨h⟩ else ∅, λ ⟨h⟩, by simp [h]⟩
id    └┘           └──────────────┘                          
src   └┘            └──────────────┘                      └────┘ 
typ   └┘           └──────────────┘                    └────┘
doc                 └──────────────┘                       └────┘ 
txt                                                        └────┘ 
par                                                        └────┘ 
pid                                                             
st                                                        └───────┘
448  
449  instance Prop.fintype : fintype Prop :=
id                           └─────┘
src                          └─────┘
typ                          └─────┘
doc                          └─────┘
450  ⟨⟨true::false::0, by simp [true_ne_false]⟩,
id     └──┘└┘└───┘└┘            └───────────┘
src    └──┘└┘└───┘└┘      └────┘└───────────┘
typ    └──┘└┘└───┘└┘      └────┘└───────────┘
doc        └┘     └┘      └────┘             
txt                       └────┘             
par                       └────┘             
pid                                        
st                       └───────────────────┘
451   classical.cases (by simp) (by simp)⟩
id    └─────────────┘
src   └─────────────┘     └──┘      └──┘
typ   └─────────────┘     └──┘      └──┘
doc                       └──┘      └──┘
txt                       └──┘      └──┘
par                       └──┘      └──┘
st                       └───┘     └───┘
452  
453  def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=
id                        └─────┘        └─┘    └────────────┘     └─────┘ 
src                       └─────┘         └─┘     └────────────┘      └─────┘
typ                       └─────┘        └─┘    └────────────┘     └─────┘ 
doc                       └─────┘                                     └─────┘
454  fintype.subtype (univ.filter (∈ s)) (by simp)
id   └─────────────┘  └──┘└─────┘   
src  └─────────────┘  └──┘└─────┘           └──┘
typ  └─────────────┘  └──┘└─────┘          └──┘
doc                   └──┘└─────┘            └──┘
txt                                          └──┘
par                                          └──┘
st                                          └───┘
455  
456  instance pi.fintype {α : Type*} {β : α → Type*}
id                                        
typ                                       
457    [fintype α] [decidable_eq α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
id      └─────┘    └──────────┘       └─────┘        └─────┘      
src     └─────┘     └──────────┘         └─────┘          └─────┘
typ     └─────┘    └──────────┘       └─────┘        └─────┘      
doc     └─────┘                          └─────┘          └─────┘
458  @fintype.of_equiv _ _
id    └──────────────┘
src   └──────────────┘
typ   └──────────────┘
doc   └──────────────┘
459    ⟨univ.pi $ λa:α, @univ (β a) _,
id      └──┘└─┘         └──┘   
src     └──┘└─┘          └──┘
typ     └──┘└─┘         └──┘   
doc     └──┘             └──┘
460      λ f, finset.mem_pi.2 $ λ a ha, mem_univ _⟩
id           └───────────┘       └┘  └──────┘
src           └───────────┘            └──────┘
typ          └───────────┘       └┘  └──────┘
461    ⟨λ f a, f a (mem_univ _), λ f a _, f a, λ f, rfl, λ f, rfl⟩
id              └──────┘                  └─┘      └─┘
src                 └──────┘                        └─┘       └─┘
typ             └──────┘                  └─┘      └─┘
462  
463  @[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
id                                                 └─────┘    └──────────┘ 
src                                                 └─────┘     └──────────┘
typ                                                └─────┘    └──────────┘ 
doc    └──┘                                         └─────┘
464    [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = univ.prod (λ a, fintype.card (β a)) :=
id              └─────┘        └──────────┘          └──┘└───┘      └──────────┘   
src              └─────┘          └──────────┘             └──┘└───┘       └──────────┘
typ             └─────┘        └──────────┘          └──┘└───┘      └──────────┘   
doc              └─────┘          └──────────┘              └──┘└───┘       └──────────┘
465  by letI f' : fintype (Πa∈univ, β a) :=
id                └─────┘     └──┘  
src     └────────┘└─────┘  └┘└──┘   └────
typ     └────────┘└─────┘  └┘└──┘  └────
doc     └────────┘└─────┘  └┘└──┘   └────
txt     └────────┘         └┘       └────
par     └────────┘         └┘       └────
pid         └─┘└─┘         └┘       └───
st     └────────────────────────────────────
466    ⟨(univ.pi $ λa, univ), assume f, finset.mem_pi.2 $ assume a ha, mem_univ _⟩;
id       └─────┘       └──┘             └───────────┘                  └──────┘
src  ─┘  └─────┘  └─┘└──┘└─┘      └──┘└───────────┘└─┘       └─────┘└──────┘└─┘
typ  ─┘  └─────┘  └─┘└──┘└─┘      └──┘└───────────┘└─┘       └─────┘└──────┘└─┘
doc  ─┘           └─┘└──┘└─┘      └──┘             └─┘       └─────┘        └─┘
txt  ─┘           └─┘    └─┘      └──┘             └─┘       └─────┘        └─┘
par  ─┘           └─┘    └─┘      └──┘             └─┘       └─────┘        └─┘
pid  ─┘           └─┘    └─┘      └──┘             └─┘       └─────┘        └─┘
st   ───────────────────────────────────────────────────────────────────────────────
467  exact calc fintype.card (Π a, β a) = fintype.card (Π a ∈ univ, β a) : fintype.card_congr
id                                                                         └────────────────┘
src  └────┘                  └┘   └┘               └───┘       └──┘└────────────────┘
typ  └────┘                  └┘   └┘               └───┘       └──┘└────────────────┘
doc  └────┘                  └┘   └┘               └───┘       └──┘                  
txt  └────┘                  └┘   └┘               └───┘       └──┘                  
par  └────┘                  └┘   └┘               └───┘       └──┘                  
pid                         └┘   └┘               └───┘       └──┘                  
st   ─────────────────────────────────────────────────────────────────────────────────────────
468    ⟨λ f a ha, f a, λ f a, f a (mem_univ a), λ _, rfl, λ _, rfl⟩
id                                 └──────┘                    └─┘
src  ─┘  └───────┘  └┘ └────┘   └──────┘ └─┘ └──┘   └┘ └──┘└─┘└─
typ  ─┘  └───────┘  └┘ └────┘   └──────┘ └─┘ └──┘   └┘ └──┘└─┘└─
doc  ─┘  └───────┘  └┘ └────┘            └─┘ └──┘   └┘ └──┘   └─
txt  ─┘  └───────┘  └┘ └────┘            └─┘ └──┘   └┘ └──┘   └─
par  ─┘  └───────┘  └┘ └────┘            └─┘ └──┘   └┘ └──┘   └─
pid  ─┘  └───────┘  └┘ └────┘            └─┘ └──┘   └┘ └──┘   └─
st   ───────────────────────────────────────────────────────────────
469  ... = univ.prod (λ a, fintype.card (β a)) : finset.card_pi _ _
id         └───────┘       └──────────┘         └────────────┘
src  ───┘ └───────┘  └──┘└──────────┘   └───┘└────────────┘└────
typ  ───┘ └───────┘  └──┘└──────────┘  └───┘└────────────┘└────
doc  ───┘ └───────┘  └──┘└──────────┘   └───┘              └────
txt  ───┘            └──┘               └───┘              └────
par  ───┘            └──┘               └───┘              └────
pid  ───┘            └──┘               └───┘              └──┘
st   ───────────────────────────────────────────────────────────────
470  
src  
typ  
doc  
txt  
par  
pid  
st   
471  @[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
id                                   └─────┘    └──────────┘    └─────┘ 
src                                  └─────┘     └──────────┘     └─────┘
typ                                  └─────┘    └──────────┘    └─────┘ 
doc    └──┘                          └─────┘                      └─────┘
472    fintype.card (α → β) = fintype.card β ^ fintype.card α :=
id     └──────────┘        └──────────┘   └──────────┘ 
src    └──────────┘          └──────────┘    └──────────┘
typ    └──────────┘        └──────────┘   └──────────┘ 
doc    └──────────┘           └──────────┘     └──────────┘
473  by rw [fintype.card_pi, finset.prod_const, nat.pow_eq_pow]; refl
id          └─────────────┘  └───────────────┘  └────────────┘
src     └──┘└─────────────┘└┘└───────────────┘└┘└────────────┘  └────
typ     └──┘└─────────────┘└┘└───────────────┘└┘└────────────┘  └────
doc     └──┘               └┘                 └┘                └────
txt     └──┘               └┘                 └┘                └────
par     └──┘               └┘                 └┘                └────
pid       └┘               └┘                 └┘                    
st     └──────────────────┘└─────────────────┘└──────────────┘└──────
474  
src  
typ  
doc  
txt  
par  
pid  
st   
475  instance d_array.fintype {n : ℕ} {α : fin n → Type*}
id                                        └─┘ 
src                                       └─┘
typ                                       └─┘ 
476    [∀n, fintype (α n)] : fintype (d_array n α) :=
id         └─────┘        └─────┘  └─────┘  
src         └─────┘          └─────┘  └─────┘
typ        └─────┘        └─────┘  └─────┘  
doc         └─────┘          └─────┘
477  fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm
id   └──────────────┘    └─────────────────────┘   └──┘
src  └──────────────┘    └─────────────────────┘   └──┘
typ  └──────────────┘    └─────────────────────┘   └──┘
doc  └──────────────┘
478  
479  instance array.fintype {n : ℕ} {α : Type*} [fintype α] : fintype (array n α) :=
id                                              └─────┘     └─────┘  └───┘  
src                                             └─────┘      └─────┘  └───┘
typ                                             └─────┘     └─────┘  └───┘  
doc                                              └─────┘      └─────┘
480  d_array.fintype
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
481  
482  instance vector.fintype {α : Type*} [fintype α] {n : ℕ} : fintype (vector α n) :=
id                                        └─────┘            └─────┘  └────┘  
src                                       └─────┘             └─────┘  └────┘
typ                                       └─────┘            └─────┘  └────┘  
doc                                       └─────┘              └─────┘
483  fintype.of_equiv _ (equiv.vector_equiv_fin _ _).symm
id   └──────────────┘    └────────────────────┘     └──┘
src  └──────────────┘    └────────────────────┘     └──┘
typ  └──────────────┘    └────────────────────┘     └──┘
doc  └──────────────┘
484  
485  @[simp] lemma card_vector [fintype α] (n : ℕ) :
id                              └─────┘        
src                             └─────┘         
typ                             └─────┘        
doc    └──┘                     └─────┘
486    fintype.card (vector α n) = fintype.card α ^ n :=
id     └──────────┘  └────┘     └──────────┘   
src    └──────────┘  └────┘       └──────────┘   
typ    └──────────┘  └────┘     └──────────┘   
doc    └──────────┘                └──────────┘
487  by rw fintype.of_equiv_card; simp
id         └───────────────────┘
src     └─┘└───────────────────┘  └────
typ     └─┘└───────────────────┘  └────
doc     └─┘                       └────
txt     └─┘                       └────
par     └─┘                       └────
pid                                  
st     └───────────────────────────────
488  
src  
typ  
doc  
txt  
par  
pid  
st   
489  instance quotient.fintype [fintype α] (s : setoid α)
id                              └─────┘        └────┘ 
src                             └─────┘         └────┘
typ                             └─────┘        └────┘ 
doc                             └─────┘
490    [decidable_rel ((≈) : α → α → Prop)] : fintype (quotient s) :=
id      └───────────┘                      └─────┘  └──────┘ 
src     └───────────┘                        └─────┘  └──────┘
typ     └───────────┘                      └─────┘  └──────┘ 
doc                                           └─────┘
491  fintype.of_surjective quotient.mk (λ x, quotient.induction_on x (λ x, ⟨x, rfl⟩))
id   └───────────────────┘ └─────────┘      └───────────────────┘          └─┘
src  └───────────────────┘ └─────────┘       └───────────────────┘             └─┘
typ  └───────────────────┘ └─────────┘      └───────────────────┘          └─┘
doc  └───────────────────┘
492  
493  instance finset.fintype [fintype α] : fintype (finset α) :=
id                            └─────┘     └─────┘  └────┘ 
src                           └─────┘      └─────┘  └────┘
typ                           └─────┘     └─────┘  └────┘ 
doc                           └─────┘      └─────┘  └────┘
494  ⟨univ.powerset, λ x, finset.mem_powerset.2 (finset.subset_univ _)⟩
id    └──┘└───────┘      └─────────────────┘   └────────────────┘
src   └──┘└───────┘       └─────────────────┘   └────────────────┘
typ   └──┘└───────┘      └─────────────────┘   └────────────────┘
doc   └──┘└───────┘
495  
496  instance subtype.fintype [fintype α] (p : α → Prop) [decidable_pred p] : fintype {x // p x} :=
id                             └─────┘                  └────────────┘     └─────┘      
src                            └─────┘                    └────────────┘      └─────┘ 
typ                            └─────┘                  └────────────┘     └─────┘      
doc                            └─────┘                                        └─────┘
497  set_fintype _
id   └─────────┘
src  └─────────┘
typ  └─────────┘
498  
499  theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
id                                    └─────┘                  └────────────┘ 
src                                   └─────┘                    └────────────┘
typ                                   └─────┘                  └────────────┘ 
doc                                   └─────┘
500    fintype.card {x // p x} ≤ fintype.card α :=
id     └──────────┘         └──────────┘ 
src    └──────────┘            └──────────┘
typ    └──────────┘         └──────────┘ 
doc    └──────────┘              └──────────┘
501  by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)
id         └──────────────────┘        └───────────────┘  └─────────┘
src     └─┘└──────────────────┘  └────┘└───────────────┘ └─────────┘└───
typ     └─┘└──────────────────┘  └────┘└───────────────┘ └─────────┘└───
doc     └─┘                      └────┘                             └───
txt     └─┘                      └────┘                             └───
par     └─┘                      └────┘                             └───
pid                                                               └─┘
st     └─────────────────────────────────────────────────────────────────
502  
src  
typ  
doc  
txt  
par  
pid  
st   
503  theorem fintype.card_subtype_lt [fintype α] {p : α → Prop} [decidable_pred p]
id                                    └─────┘                  └────────────┘ 
src                                   └─────┘                    └────────────┘
typ                                   └─────┘                  └────────────┘ 
doc                                   └─────┘
504    {x : α} (hx : ¬ p x) : fintype.card {x // p x} < fintype.card α :=
id                        └──────────┘         └──────────┘ 
src                          └──────────┘            └──────────┘
typ                       └──────────┘         └──────────┘ 
doc                           └──────────┘              └──────────┘
505  by rw [fintype.subtype_card]; exact finset.card_lt_card
id          └──────────────────┘         └─────────────────┘
src     └──┘└──────────────────┘  └────┘└─────────────────┘
typ     └──┘└──────────────────┘  └────┘└─────────────────┘
doc     └──┘                      └────┘                   
txt     └──┘                      └────┘                   
par     └──┘                      └────┘                   
pid       └┘                                              
st     └───────────────────────┘└───────────────────────────
506    ⟨subset_univ _, classical.not_forall.2 ⟨x, by simp [*, set.mem_def]⟩⟩
id      └─────────┘    └──────────────────┘                  └─────────┘
src  ─┘ └─────────┘└──┘└──────────────────┘└─┘  └┘  └───────┘└─────────┘└──
typ  ─┘ └─────────┘└──┘└──────────────────┘└─┘ └┘  └───────┘└─────────┘└──
doc  ─┘            └──┘                    └─┘  └┘  └───────┘           └──
txt  ─┘            └──┘                    └─┘  └┘  └───────┘           └──
par  ─┘            └──┘                    └─┘  └┘  └───────┘           └──
pid  ─┘            └──┘                    └─┘  └┘  └────────┘           └─┘
st   ──────────────────────────────────────────────┘└────────────────────┘└──
507  
src  
typ  
doc  
txt  
par  
pid  
st   
508  instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
id                                                       └─────┘        └─────┘   
src                                                       └─────┘          └─────┘
typ                                                      └─────┘        └─────┘   
doc                                                       └─────┘          └─────┘
509    fintype (Σ' a, β a) :=
id     └─────┘  └┘   
src    └─────┘  └┘  
typ    └─────┘  └┘   
doc    └─────┘
510  fintype.of_equiv _ (equiv.psigma_equiv_sigma _).symm
id   └──────────────┘    └──────────────────────┘   └──┘
src  └──────────────┘    └──────────────────────┘   └──┘
typ  └──────────────┘    └──────────────────────┘   └──┘
doc  └──────────────┘
511  
512  instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [∀ a, fintype (β a)] [decidable α] :
id                                                                    └─────┘       └───────┘ 
src                                                                     └─────┘         └───────┘
typ                                                                   └─────┘       └───────┘ 
doc                                                                     └─────┘
513    fintype (Σ' a, β a) :=
id     └─────┘  └┘   
src    └─────┘  └┘  
typ    └─────┘  └┘   
doc    └─────┘
514  if h : α then fintype.of_equiv (β h) ⟨λ x, ⟨h, x⟩, psigma.snd, λ _, rfl, λ ⟨_, _⟩, rfl⟩
id   └┘           └──────────────┘                └────────┘      └─┘           └─┘
src  └┘            └──────────────┘                     └────────┘       └─┘            └─┘
typ  └┘           └──────────────┘                └────────┘      └─┘           └─┘
doc                └──────────────┘
515  else ⟨∅, λ x, h x.1⟩
id               
src                  
typ              
516  
517  instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [fintype α] [∀ a, decidable (β a)] :
id                                                                 └─────┘        └───────┘   
src                                                                 └─────┘          └───────┘
typ                                                                └─────┘        └───────┘   
doc                                                                 └─────┘
518    fintype (Σ' a, β a) :=
id     └─────┘  └┘   
src    └─────┘  └┘  
typ    └─────┘  └┘   
doc    └─────┘
519  fintype.of_equiv {a // β a} ⟨λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, rfl, λ ⟨x, y⟩, rfl⟩
id   └──────────────┘                                                └─┘           └─┘
src  └──────────────┘                                                          └─┘            └─┘
typ  └──────────────┘                                                └─┘           └─┘
doc  └──────────────┘
520  
521  instance psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [∀ a, decidable (β a)] :
id                                                               └───────┘        └───────┘   
src                                                               └───────┘          └───────┘
typ                                                              └───────┘        └───────┘   
522    fintype (Σ' a, β a) :=
id     └─────┘  └┘   
src    └─────┘  └┘  
typ    └─────┘  └┘   
doc    └─────┘
523  if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, λ ⟨_, _⟩, by simp⟩ else ⟨∅, λ ⟨x, y⟩, h ⟨x, y⟩⟩
id   └┘                └──┘  └──┘                                    
src  └┘                    └──┘   └──┘                 └──┘        
typ  └┘                └──┘  └──┘                └──┘                
doc                                                       └──┘
txt                                                       └──┘
par                                                       └──┘
st                                                       └───┘
524  
525  instance set.fintype [fintype α] [decidable_eq α] : fintype (set α) :=
id                         └─────┘    └──────────┘     └─────┘  └─┘ 
src                        └─────┘     └──────────┘      └─────┘  └─┘
typ                        └─────┘    └──────────┘     └─────┘  └─┘ 
doc                        └─────┘                       └─────┘
526  pi.fintype
id   └────────┘
src  └────────┘
typ  └────────┘
527  
528  instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)
id                                     └───────┘        
src                                    └───────┘
typ                                    └───────┘        
529    [Π hp, fintype (α hp)] : fintype (Π hp : p, α hp) :=
id        └┘  └─────┘   └┘     └─────┘            └┘
src           └─────┘           └─────┘
typ       └┘  └─────┘   └┘     └─────┘            └┘
doc           └─────┘           └─────┘
530  if hp : p then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl⟩
id   └┘            └──────────────┘   └┘               └┘      └─┘      └─┘
src  └┘             └──────────────┘                                   └─┘       └─┘
typ  └┘            └──────────────┘   └┘               └┘      └─┘      └─┘
doc                 └──────────────┘
531            else ⟨singleton (λ h, (hp h).elim), by simp [hp, function.funext_iff]⟩
id                  └───────┘       └┘  └──┘             └┘  └─────────────────┘
src                  └───────┘             └──┘       └────┘  └┘└─────────────────┘
typ                 └───────┘       └┘  └──┘       └────┘└┘└┘└─────────────────┘
doc                  └───────┘                        └────┘  └┘                   
txt                                                   └────┘  └┘                   
par                                                   └────┘  └┘                   
pid                                                         └┘                   
st                                                   └─────────────────────────────┘
532  
533  def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
id                                            └──────────┘ 
src                                           └──────────┘
typ                                           └──────────┘ 
534    {α : ι → Type*} [S : ∀ i, setoid (α i)] :
id                             └────┘   
src                              └────┘
typ                            └────┘   
535    ∀ (l : list ι), (∀ i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
id           └──┘            └──────┘         └──────┘          
src           └──┘               └──────┘           └──────┘                    └────────────┘
typ          └──┘            └──────┘         └──────┘                └────────────┘
doc                                                                             └────────────┘
txt                                                                             └────────────┘
par                                                                             └────────────┘
st                                                                             └─────────────┘
536  | []     f := ⟦λ i, false.elim⟧
id     └┘              └────────┘
src    └┘               └────────┘
typ    └┘              └────────┘
537  | (i::l) f := begin
id       └┘
src      └┘
typ      └┘
st                 └─────
538    refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
id            └───────────────┘      └────────────────┘
src    └─────┘└───────────────┘    └────────────────┘└──────
typ    └─────┘└───────────────┘   └────────────────┘└──────
doc    └─────┘                                       └──────
txt    └─────┘                                       └──────
par    └─────┘                                       └──────
pid                                                 └──────
st   ──────────────────────────────────────────────────────────
539      (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
id        └─────────────────────┘              └──────────────────┘
src  ───┘                           └────┘   └──────────────────┘└─┘ └───
typ  ───┘ └─────────────────────┘  └────┘  └──────────────────┘└─┘ └───
doc  ───┘                           └────┘                       └─┘ └───
txt  ───┘                           └────┘                       └─┘ └───
par  ───┘                           └────┘                       └─┘ └───
pid  ───┘                           └────┘                       └─┘ └───
st   ────────────────────────────────────────────────────────────────────────
540      _ _,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘└─
541    exact λ a l, ⟦λ j h,
id                  
src    └────┘ └────┘ └─────
typ    └────┘ └────┘ └─────
doc    └────┘ └────┘  └─────
txt    └────┘ └────┘  └─────
par    └────┘ └────┘  └─────
pid          └────┘  └─────
st   ───────────────────────
542      if e : j = i then by rw e; exact a else
id       └┘                            
src  ───┘└┘└───┘  └────┘  └─┘ └──────┘ └─────
typ  ───┘└┘└───┘ └────┘  └─┘└──────┘└─────
doc  ───┘  └───┘   └────┘  └─┘ └──────┘ └─────
txt  ───┘  └───┘   └────┘  └─┘ └──────┘ └─────
par  ───┘  └───┘   └────┘  └─┘ └──────┘ └─────
pid  ───┘  └───┘   └────┘  └──┘ └──────┘ └─────
st   ───────────────────────┘└─────────────┘└────
543      l _ (h.resolve_left e)⟧,
id            └───────────┘   
src  ───┘ └─┘  └───────────┘ 
typ  ───┘└─┘  └───────────┘ 
doc  ───┘ └─┘                
txt  ───┘ └─┘                
par  ───┘ └─┘                
pid  ───┘ └─┘                
st   ──────────────────────────┘└─
544    refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
id                                 └────────────┘
src    └─────┘ └──────────────────┘└────────────┘  └──────┘
typ    └─────┘ └──────────────────┘└────────────┘  └──────┘
doc    └─────┘ └──────────────────┘                └──────┘
txt    └─────┘ └──────────────────┘                └──────┘
par    └─────┘ └──────────────────┘                └──────┘
pid           └──────────────────┘                └──────┘
st   ──────────────────────────────────────────────────────┘└─
545    by_cases e : j = i; simp [e],
id                             
src    └───────┘ └─┘     └────┘ 
typ    └───────┘ └─┘   └────┘
doc    └───────┘ └─┘     └────┘ 
txt    └───────┘ └─┘     └────┘ 
par    └───────┘ └─┘     └────┘ 
pid             └─┘          
st   ─────────────────────────────┘└─
546    { subst j, exact h₁ },
id                     └┘
src      └────┘   └────┘  
typ      └────┘  └────┘└┘
doc      └────┘   └────┘  
txt      └────┘   └────┘  
par      └────┘   └────┘  
pid                     
st   ───┘└─────┘└─────────┘└┘
547    { exact h₂ _ _ }
id             └┘
src      └────┘  └───┘
typ      └────┘└┘└───┘
doc      └────┘  └───┘
txt      └────┘  └───┘
par      └────┘  └───┘
pid             └──┘
st   ────────────────┘└─
548  end
st   ──┘
549  
550  theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
id                                                   └──────────┘ 
src                                                  └──────────┘
typ                                                  └──────────┘ 
551    {α : ι → Type*} [S : ∀ i, setoid (α i)] :
id                             └────┘   
src                              └────┘
typ                            └────┘   
552    ∀ (l : list ι) (f : ∀ i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
id           └──┘                   └─────────────────────┘             
src           └──┘                        └─────────────────────┘                    
typ          └──┘                   └─────────────────────┘             
553  | []     f := quotient.sound (λ i h, h.elim)
id     └┘          └────────────┘       └───┘
src    └┘          └────────────┘          └───┘
typ    └┘          └────────────┘       └───┘
554  | (i::l) f := begin
id       └┘
src      └┘
typ      └┘
st                 └─────
555    simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
id           └─────────────────────┘  └────────────────────────┘ 
src    └────┘└─────────────────────┘└┘                           
typ    └────┘└─────────────────────┘└┘└────────────────────────┘
doc    └────┘                       └┘                           
txt    └────┘                       └┘                           
par    └────┘                       └┘                           
pid                               └┘                           
st   ─────────────────────────────────────────────────────────────┘└─
556    refine quotient.sound (λ j h, _),
id            └────────────┘
src    └─────┘└────────────┘  └──────┘
typ    └─────┘└────────────┘  └──────┘
doc    └─────┘                └──────┘
txt    └─────┘                └──────┘
par    └─────┘                └──────┘
pid                          └──────┘
st   ─────────────────────────────────┘└─
557    by_cases e : j = i; simp [e],
id                            
src    └───────┘ └─┘    └────┘ 
typ    └───────┘ └─┘  └────┘
doc    └───────┘ └─┘     └────┘ 
txt    └───────┘ └─┘     └────┘ 
par    └───────┘ └─┘     └────┘ 
pid             └─┘          
st   ─────────────────────────────┘└─
558    subst j, refl
id           
src    └────┘   └───┘
typ    └────┘  └───┘
doc    └────┘   └───┘
txt    └────┘   └───┘
par    └────┘   └───┘
pid                
st   ────────┘└─────┘
559  end
st   └─┘
560  
561  def quotient.fin_choice {ι : Type*} [fintype ι] [decidable_eq ι]
id                                        └─────┘    └──────────┘ 
src                                       └─────┘     └──────────┘
typ                                       └─────┘    └──────────┘ 
doc                                       └─────┘
562    {α : ι → Type*} [S : ∀ i, setoid (α i)]
id                             └────┘   
src                              └────┘
typ                            └────┘   
563    (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
id              └──────┘         └──────┘       
src              └──────┘           └──────┘                └────────────┘
typ             └──────┘         └──────┘             └────────────┘
doc                                                         └────────────┘
txt                                                         └────────────┘
par                                                         └────────────┘
st                                                         └─────────────┘
564  quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
id   └──────────────┘   └─────────────┘            └──────┘ 
src  └──────────────┘   └─────────────┘            └──────┘
typ  └──────────────┘   └─────────────┘            └──────┘ 
doc                                                └──────┘
565      @quotient (Π i ∈ l, α i) (by apply_instance))
id        └──────┘          
src       └──────┘                    └────────────┘
typ       └──────┘                └────────────┘
doc                                   └────────────┘
txt                                   └────────────┘
par                                   └────────────┘
st                                   └─────────────┘
566      finset.univ.1
id       └─────────┘
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
567      (λ l, quotient.fin_choice_aux l (λ i _, f i))
id            └─────────────────────┘         
src            └─────────────────────┘
typ           └─────────────────────┘         
568      (λ a b h, begin
id            
typ           
st                 └─────
569        have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
id                      └────────────────────────┘           └──────────┘  
src        └──────┘ └──┘└────────────────────────┘   └────┘└──────────┘   └┘
typ        └──────┘ └──┘└────────────────────────┘   └────┘└──────────┘  └┘
doc        └──────┘ └──┘                             └────┘└──────────┘   └┘
txt        └──────┘ └──┘                             └────┘               └┘
par        └──────┘ └──┘                             └────┘               └┘
pid        └───┘└─┘ └──┘                             └────┘               └┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
570        simp [quotient.out_eq] at this,
id               └─────────────┘
src        └────┘└─────────────┘└───────┘
typ        └────┘└─────────────┘└───────┘
doc        └────┘               └───────┘
txt        └────┘               └───────┘
par        └────┘               └───────┘
pid                           └─────┘
st   ───────────────────────────────────┘└─
571        simp [this],
id               └──┘
src        └────┘    
typ        └────┘└──┘
doc        └────┘    
txt        └────┘    
par        └────┘    
pid                
st   ────────────────┘└─
572        let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
id                      └──────┘                         └──────────┘     
src        └───────┘ └─┘└──────┘ └┘ └────┘ └─────┘  └─┘└──────────┘   
typ        └───────┘ └─┘└──────┘ └┘ └────┘└─────┘  └─┘└──────────┘  
doc        └───────┘ └─┘└──────┘ └┘  └────┘ └─────┘   └─┘└──────────┘   
txt        └───────┘ └─┘         └┘  └────┘ └─────┘   └─┘               
par        └───────┘ └─┘         └┘  └────┘ └─────┘   └─┘               
pid        └───┘└─┘ └─┘         └┘  └────┘ └─────┘   └─┘               
st   ─────────────────────────────────────────────────────────────────────────┘└─
573        refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
id                └───────┘   └────────┘                    └┘  
src        └─────┘└───────┘  └────────┘└──────────┘ └──┘  └┘  └┘
typ        └─────┘└───────┘  └────────┘└──────────┘ └──┘ └┘└┘
doc        └─────┘                     └──────────┘ └──┘      └┘
txt        └─────┘                     └──────────┘ └──┘      └┘
par        └─────┘                     └──────────┘ └──┘      └┘
pid                                   └──────────┘ └──┘      └┘
st   ───────────────────────────────────────────────────────────────┘└─
574        congr' 1, exact quotient.sound h,
id                         └────────────┘ 
src        └──────┘  └────┘└────────────┘
typ        └──────┘  └────┘└────────────┘
doc        └──────┘  └────┘              
txt        └──────┘  └────┘              
par        └──────┘  └────┘              
pid                                   
st   ─────────────┘└──────────────────────┘└─
575      end))
st   ──────┘
576    (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
id                 └─────────────┘   
src                    └─────────────┘   
typ                └─────────────┘   
577    (λ a b h, quotient.sound $ λ i, h _ _)
id            └────────────┘       
src              └────────────┘
typ           └────────────┘       
578  
579  theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
id                                               └─────┘    └──────────┘ 
src                                              └─────┘     └──────────┘
typ                                              └─────┘    └──────────┘ 
doc                                              └─────┘
580    {α : ι → Type*} [∀ i, setoid (α i)]
id                         └────┘   
src                          └────┘
typ                        └────┘   
581    (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
id                   └─────────────────┘          
src                     └─────────────────┘              
typ                  └─────────────────┘          
582  begin
st   └─────
583    let q, swap, change quotient.lift_on q _ _ = _,
id                         └──────────────┘      
src    └───┘  └──┘  └─────┘└──────────────┘ └───┘└┘
typ    └───┘  └──┘  └─────┘└──────────────┘└───┘└┘
doc    └───┘  └──┘  └─────┘                 └───┘ └┘
txt    └───┘  └──┘  └─────┘                 └───┘ └┘
par    └───┘  └──┘  └─────┘                 └───┘ └┘
pid    └───┘                               └───┘ └┘
st   ──────┘└────┘└─────────────────────────────────┘└─
584    have : q = ⟦λ i h, f i⟧,
id                        
src    └─────┘   └────┘  
typ    └─────┘  └────┘ 
doc    └─────┘    └────┘ 
txt    └─────┘    └────┘ 
par    └─────┘    └────┘ 
pid    └───┘└┘    └────┘ 
st   ────────────────────────┘└─
585    { dsimp [q],
id              
src      └─────┘ 
typ      └─────┘
doc      └─────┘ 
txt      └─────┘ 
par      └─────┘ 
pid            
st   ───┘└───────┘└─
586      exact quotient.induction_on
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ────────────────────────────────
587        (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
id           └─────────┘             └────────────────────────┘
src  ─────┘  └─────────┘ └────┘  └──┘└────────────────────────┘└────┘
typ  ─────┘  └─────────┘└────┘  └──┘└────────────────────────┘└────┘
doc  ─────┘  └─────────┘ └────┘  └──┘                          └────┘
txt  ─────┘              └────┘  └──┘                          └────┘
par  ─────┘              └────┘  └──┘                          └────┘
pid  ─────┘              └────┘  └──┘                          └───┘
st   ────────────────────────────────────────────────────────────────┘└┘
588    simp [this], exact setoid.refl _
id           └──┘         └─────────┘
src    └────┘      └────┘└─────────┘└─┘
typ    └────┘└──┘  └────┘└─────────┘└─┘
doc    └────┘      └────┘           └─┘
txt    └────┘      └────┘           └─┘
par    └────┘      └────┘           └─┘
pid                              └┘
st   ────────────┘└────────────────────┘
589  end
st   └─┘
590  
591  @[simp, to_additive]
doc    └──┘  └─────────┘
592  lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
id                                  └─────┘    └─────────┘                   └──┘       
src                                 └─────┘     └─────────┘                      └──┘
typ                                 └─────┘    └─────────┘                   └──┘       
doc                                 └─────┘                                        └──┘
593    univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) :=
id     └──┘└─────┘└───┘          └──┘└───┘           └──────┘
src    └──┘└─────┘└───┘             └──┘└───┘              └──────┘
typ    └──┘└─────┘└───┘          └──┘└───┘           └──────┘
doc    └──┘└─────┘└───┘              └──┘└───┘
594  prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
id   └──────┘                └──────┘                                        └──────┘
src  └──────┘                     └──────┘                └──┘      └──┘               └──────┘        └──┘
typ  └──────┘                └──────┘              └──┘      └──┘            └──────┘        └──┘
doc                                                        └──┘      └──┘                               └──┘
txt                                                        └──┘      └──┘                               └──┘
par                                                        └──┘      └──┘                               └──┘
st                                                        └───┘     └───┘                              └───┘
595  
596  @[to_additive]
doc    └─────────┘
597  lemma finset.range_prod_eq_univ_prod [comm_monoid β] (n : ℕ) (f : ℕ → β) :
id                                         └─────────┘                  
src                                        └─────────┘                
typ                                        └─────────┘                  
598    (range n).prod f = univ.prod (λ (k : fin n), f k) :=
id      └───┘  └──┘    └──┘└───┘         └─┘     
src     └───┘   └──┘     └──┘└───┘         └─┘
typ     └───┘  └──┘    └──┘└───┘         └─┘     
doc     └───┘   └──┘      └──┘└───┘
599  begin
st   └─────
600    symmetry,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
st   ─────────┘└─
601    refine prod_bij (λ k hk, k) _ _ _ _,
id            └──────┘
src    └─────┘└──────┘  └─────┘ └───────┘
typ    └─────┘└──────┘  └─────┘ └───────┘
doc    └─────┘          └─────┘ └───────┘
txt    └─────┘          └─────┘ └───────┘
par    └─────┘          └─────┘ └───────┘
pid                    └─────┘ └───────┘
st   ────────────────────────────────────┘└─
602    { rintro ⟨k, hk⟩ _, simp * },
src      └──────────────┘  └─────┘
typ      └──────────────┘  └─────┘
doc      └──────────────┘  └─────┘
txt      └──────────────┘  └─────┘
par      └──────────────┘  └─────┘
pid            └────────┘      
st   ───┘└──────────────┘└───────┘└┘
603    { rintro ⟨k, hk⟩ _, simp * },
src      └──────────────┘  └─────┘
typ      └──────────────┘  └─────┘
doc      └──────────────┘  └─────┘
txt      └──────────────┘  └─────┘
par      └──────────────┘  └─────┘
pid            └────────┘      
st   ───┘└──────────────┘└───────┘└┘
604    { intros, rwa fin.eq_iff_veq },
id                   └────────────┘
src      └────┘  └──┘└────────────┘
typ      └────┘  └──┘└────────────┘
doc      └────┘  └──┘              
txt      └────┘  └──┘              
par      └────┘  └──┘              
pid                               
st   ───┘└────┘└───────────────────┘└┘
605    { intros k hk, rw mem_range at hk,
id                       └───────┘
src      └─────────┘  └─┘└───────┘└────┘
typ      └─────────┘  └─┘└───────┘└────┘
doc      └─────────┘  └─┘         └────┘
txt      └─────────┘  └─┘         └────┘
par      └─────────┘  └─┘         └────┘
pid            └───┘             └────┘
st   ──────────────┘└──────────────────┘└─
606      exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
id                 └┘   └──────┘    └─┘
src      └────┘   └┘  └─┘└──────┘└──┘└─┘└┘
typ      └────┘  └┘└┘└─┘└──────┘└──┘└─┘└┘
doc      └────┘   └┘  └─┘        └──┘   └┘
txt      └────┘   └┘  └─┘        └──┘   └┘
par      └────┘   └┘  └─┘        └──┘   └┘
pid              └┘  └─┘        └──┘   
st   ────────────────────────────────────┘└─
607  end
st   ──┘
608  
609  section equiv
610  
611  open list equiv equiv.perm
612  
613  variables [decidable_eq α] [decidable_eq β]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
614  
615  def perms_of_list : list α → list (perm α)
id                       └──┘   └──┘  └──┘ 
src                      └──┘     └──┘  └──┘
typ                      └──┘   └──┘  └──┘ 
doc                                     └──┘
616  | []       := [1]
id     └┘           
src    └┘           
typ    └┘           
617  | (a :: l) := perms_of_list l ++ l.bind (λ b, (perms_of_list l).map (λ f, swap a b * f))
id       └┘      └───────────┘   └┘  └───┘       └───────────┘   └─┘       └──┘     
src       └┘                       └┘  └───┘                        └─┘        └──┘     
typ      └┘      └───────────┘   └┘  └───┘       └───────────┘   └─┘       └──┘     
doc                                                                            └──┘
618  
619  lemma length_perms_of_list : ∀ l : list α, length (perms_of_list l) = l.length.fact
id                                     └──┘   └────┘  └───────────┘    └─────┘└───┘
src                                     └──┘    └────┘  └───────────┘      └─────┘└───┘
typ                                    └──┘   └────┘  └───────────┘    └─────┘└───┘
doc                                                                                └───┘
620  | []       := rfl
id     └┘          └─┘
src    └┘          └─┘
typ    └┘          └─┘
621  | (a :: l) := by rw [length_cons, nat.fact_succ];
id        └┘              └─────────┘  └───────────┘
src       └┘          └──┘└─────────┘└┘└───────────┘
typ       └┘          └──┘└─────────┘└┘└───────────┘
doc                   └──┘           └┘             
txt                   └──┘           └┘             
par                   └──┘           └┘             
pid                     └┘           └┘             
st                   └──────────────┘└─────────────┘└─
622    simp [perms_of_list, length_bind, length_perms_of_list, function.comp, nat.succ_mul]
id           └───────────┘  └─────────┘  └──────────────────┘  └───────────┘  └──────────┘
src    └────┘└───────────┘└┘└─────────┘└┘                    └┘└───────────┘└┘└──────────┘└─
typ    └────┘└───────────┘└┘└─────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘└─
doc    └────┘             └┘           └┘                    └┘             └┘            └─
txt    └────┘             └┘           └┘                    └┘             └┘            └─
par    └────┘             └┘           └┘                    └┘             └┘            └─
pid                     └┘           └┘                    └┘             └┘            
st   ───────────────────────────────────────────────────────────────────────────────────────
623  
src  
typ  
doc  
txt  
par  
pid  
st   
624  lemma mem_perms_of_list_of_mem : ∀ {l : list α} {f : perm α} (h : ∀ x, f x ≠ x → x ∈ l), f ∈ perms_of_list l
id                                          └──┘        └──┘                         └───────────┘ 
src                                          └──┘         └──┘                                 └───────────┘
typ                                         └──┘        └──┘                         └───────────┘ 
doc                                                       └──┘
625  | []     f h := list.mem_singleton.2 $ equiv.ext _ _$ λ x, by simp [imp_false, *] at *
id     └┘            └────────────────┘    └───────┘                   └───────┘
src    └┘            └────────────────┘    └───────┘              └────┘└───────┘└────────┘
typ    └┘            └────────────────┘    └───────┘             └────┘└───────┘└────────┘
doc                                                                └────┘         └────────┘
txt                                                                └────┘         └────────┘
par                                                                └────┘         └────────┘
pid                                                                             └──┘└──┘
st                                                                └────────────────────────┘
626  | (a::l) f h :=
id      └┘   
src      └┘
typ     └┘   
627  if hfa : f a = a
id   └┘           
src  └┘           
typ  └┘           
628  then
629    mem_append_left _ $ mem_perms_of_list_of_mem
id     └─────────────┘     └──────────────────────┘
src    └─────────────┘
typ    └─────────────┘     └──────────────────────┘
630      (λ x hx, mem_of_ne_of_mem (λ h, by rw h at hx; exact hx hfa) (h x hx))
id           └┘  └──────────────┘                          └┘ └─┘      └┘
src               └──────────────┘          └─┘ └────┘  └────┘  
typ          └┘  └──────────────┘         └─┘└────┘  └────┘└┘└─┘      └┘
doc                                         └─┘ └────┘  └────┘  
txt                                         └─┘ └────┘  └────┘  
par                                         └─┘ └────┘  └────┘  
pid                                            └────┘         
st                                         └───────────────────────┘
631  else
632  have hfa' : f (f a) ≠ f a, from mt (λ h, f.injective h) hfa,
id   └──┘                           └┘       └────────┘   └─┘
src                                 └┘        └────────┘
typ  └──┘                           └┘       └────────┘   └─┘
633  have ∀ (x : α), (swap a (f a) * f) x ≠ x → x ∈ l,
id                   └──┘                   
src                   └──┘                      
typ                  └──┘                   
doc                   └──┘
634    from λ x hx, have hxa : x ≠ a, from λ h, by simpa [h, mul_apply] using hx,
id             └┘                                       └───────┘        └┘
src                                               └─────┘ └┘└───────┘└──────┘
typ            └┘                              └─────┘└┘└───────┘└──────┘└┘
doc                                                └─────┘ └┘         └──────┘
txt                                                └─────┘ └┘         └──────┘
par                                                └─────┘ └┘         └──────┘
pid                                                      └┘         └────┘
st                                                └────────────────────────────┘
635      have hfxa : f x ≠ f a, from mt (λ h, f.injective h) hxa,
id                                 └┘       └────────┘   └─┘
src                                 └┘        └────────┘
typ                                └┘       └────────┘   └─┘
636      list.mem_of_ne_of_mem hxa
id       └───────────────────┘ └─┘
src      └───────────────────┘
typ      └───────────────────┘ └─┘
637        (h x (λ h, by simp [h, mul_apply, swap_apply_def] at hx; split_ifs at hx; cc)),
id                             └───────┘  └────────────┘
src                      └────┘ └┘└───────┘└┘└────────────┘└─────┘  └─────────────┘  └┘
typ                    └────┘└┘└───────┘└┘└────────────┘└─────┘  └─────────────┘  └┘
doc                      └────┘ └┘         └┘              └─────┘  └─────────────┘  └┘
txt                      └────┘ └┘         └┘              └─────┘  └─────────────┘  └┘
par                      └────┘ └┘         └┘              └─────┘  └─────────────┘  └┘
pid                           └┘         └┘              └───┘           └────┘
st                      └─────────────────────────────────────────────────────────────┘
638  suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g ∈ perms_of_list l ∧ swap a b * g = f,
id               └───────────┘                      └──┘    └───────────┘    └──┘      
src              └───────────┘                        └──┘      └───────────┘    └──┘        
typ              └───────────┘                      └──┘    └───────────┘    └──┘      
doc                                                          └──┘                          └──┘
639    by simpa [perms_of_list],
id               └───────────┘
src       └─────┘└───────────┘
typ       └─────┘└───────────┘
doc       └─────┘             
txt       └─────┘             
par       └─────┘             
pid                         
st       └────────────────────┘
640  (@or_iff_not_imp_left _ _ (classical.prop_decidable _)).2
id     └─────────────────┘      └──────────────────────┘    
src    └─────────────────┘      └──────────────────────┘    
typ    └─────────────────┘      └──────────────────────┘    
641    (λ hfl, ⟨f a,
id        └─┘
typ       └─┘
642      if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.injective h) hfa))
id       └┘                        └──────────────┘ └─┘       └┘       └────────┘   └─┘
src      └┘                        └──────────────┘           └┘        └────────┘
typ      └┘                        └──────────────┘ └─┘       └┘       └────────┘   └─┘
643        else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
id              └──┘             └───────┘  └────────────┘
src                         └────┘└───────┘└┘└────────────┘  └───────┘  └┘
typ             └──┘       └────┘└───────┘└┘└────────────┘  └───────┘  └┘
doc                         └────┘         └┘                └───────┘  └┘
txt                         └────┘         └┘                └───────┘  └┘
par                         └────┘         └┘                └───────┘  └┘
pid                                      └┘              
st                         └──────────────────────────────────────────────┘
644      ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
id        └──┘             └──────────────────────┘ └──┘
src       └──┘         
typ       └──┘             └──────────────────────┘ └──┘
doc       └──┘
645        by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← equiv.perm.one_def, one_mul]⟩⟩)
id                  └───────┘  └─────┘                 └──┘         └───────┘    └────────────────┘  └─────┘
src           └────┘└───────┘└┘└─────┘         └─┘ └──┘    └──┘└───────┘└──┘└────────────────┘└┘└─────┘
typ           └────┘└───────┘└┘└─────┘         └─┘ └──┘  └──┘└───────┘└──┘└────────────────┘└┘└─────┘
doc           └────┘         └┘                └─┘ └──┘    └──┘         └──┘                  └┘       
txt           └────┘         └┘                └─┘         └──┘         └──┘                  └┘       
par           └────┘         └┘                └─┘         └──┘         └──┘                  └┘       
pid             └──┘         └┘                └─┘         └──┘         └──┘                  └┘       
st           └──────────────┘└─────────────────────────────────────┘└─────────┘└────────────────────┘└───────┘
646  
647  lemma mem_of_mem_perms_of_list : ∀ {l : list α} {f : perm α}, f ∈ perms_of_list l → ∀ {x}, f x ≠ x → x ∈ l
id                                          └──┘        └──┘      └───────────┘                  
src                                          └──┘         └──┘        └───────────┘                       
typ                                         └──┘        └──┘      └───────────┘                  
doc                                                       └──┘
648  | []     f h := have f = 1 := by simpa [perms_of_list] using h, by rw this; simp
id     └┘                                  └───────────┘                └──┘
src    └┘                            └─────┘└───────────┘└──────┘      └─┘      └───┘
typ    └┘                           └─────┘└───────────┘└──────┘     └─┘└──┘  └───┘
doc                                   └─────┘             └──────┘      └─┘      └───┘
txt                                   └─────┘             └──────┘      └─┘      └───┘
par                                   └─────┘             └──────┘      └─┘      └───┘
pid                                                     └────┘                  
st                                   └────────────────────────────┘    └─────────────┘
649  | (a::l) f h :=
id      └┘     
src      └┘
typ     └┘     
650  (mem_append.1 h).elim
id    └────────┘    └──┘
src   └────────┘    └──┘
typ   └────────┘    └──┘
651    (λ h x hx, mem_cons_of_mem _ (mem_of_mem_perms_of_list h hx))
id          └┘  └─────────────┘    └──────────────────────┘  └┘
src               └─────────────┘
typ         └┘  └─────────────┘    └──────────────────────┘  └┘
652    (λ h x hx,
id          └┘
typ         └┘
653      let ⟨y, hy, hy'⟩ := list.mem_bind.1 h in
id       └─┘        └─┘     └───────────┘  
src                          └───────────┘
typ      └─┘        └─┘     └───────────┘  
654      let ⟨g, hg₁, hg₂⟩ := list.mem_map.1 hy' in
id       └─┘     └─┘          └──────────┘
src                           └──────────┘
typ      └─┘     └─┘          └──────────┘
655      if hxa : x = a then by simp [hxa]
id       └┘                         └─┘
src      └┘                    └────┘   └─
typ      └┘                   └────┘└─┘└─
doc                             └────┘   └─
txt                             └────┘   └─
par                             └────┘   └─
pid                                    
st                             └───────────
656      else if hxy : x = y then mem_cons_of_mem _ $ by rwa hxy
id            └┘                └─────────────┘            └─┘
src  ───┘     └┘                 └─────────────┘        └──┘   
typ  ───┘     └┘                └─────────────┘        └──┘└─┘
doc  ───┘                                                └──┘   
txt  ───┘                                                └──┘   
par  ───┘                                                └──┘   
pid  ───┘                                                      
st   ───┘                                               └────────
657      else mem_cons_of_mem _ $
id            └─────────────┘   
src  ───┘     └─────────────┘
typ  ───┘     └─────────────┘   
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
658      mem_of_mem_perms_of_list hg₁ $
id       └──────────────────────┘
typ      └──────────────────────┘
659        by rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def];
id                └───────────────────┘   └─┘  └───────┘  └──────┘  └────────────┘
src           └──┘└───────────────────┘└─┘   └┘└───────┘└┘└──────┘└┘└────────────┘
typ           └──┘└───────────────────┘└─┘└─┘└┘└───────┘└┘└──────┘└┘└────────────┘
doc           └──┘                     └─┘   └┘         └┘        └┘              
txt           └──┘                     └─┘   └┘         └┘        └┘              
par           └──┘                     └─┘   └┘         └┘        └┘              
pid             └┘                     └─┘   └┘         └┘        └┘              
st           └──────────────────────────────┘└─────────┘└────────┘└──────────────┘└─
660          split_ifs; cc)
src          └───────┘  └┘
typ          └───────┘  └┘
doc          └───────┘  └┘
txt          └───────┘  └┘
par          └───────┘  └┘
st   ────────────────────┘
661  
662  lemma mem_perms_of_list_iff {l : list α} {f : perm α} : f ∈ perms_of_list l ↔ ∀ {x}, f x ≠ x → x ∈ l :=
id                                    └──┘        └──┘       └───────────┘                 
src                                   └──┘         └──┘         └───────────┘                      
typ                                   └──┘        └──┘       └───────────┘                 
doc                                                └──┘
663  ⟨mem_of_mem_perms_of_list, mem_perms_of_list_of_mem⟩
id    └──────────────────────┘  └──────────────────────┘
src   └──────────────────────┘  └──────────────────────┘
typ   └──────────────────────┘  └──────────────────────┘
664  
665  lemma nodup_perms_of_list : ∀ {l : list α} (hl : l.nodup), (perms_of_list l).nodup
id                                     └──┘         └────┘    └───────────┘  └───┘
src                                     └──┘           └────┘    └───────────┘   └───┘
typ                                    └──┘         └────┘    └───────────┘  └───┘
doc                                                    └────┘                    └───┘
666  | []     hl := by simp [perms_of_list]
id     └┘                    └───────────┘
src    └┘              └────┘└───────────┘└┘
typ    └┘              └────┘└───────────┘└┘
doc                    └────┘             └┘
txt                    └────┘             └┘
par                    └────┘             └┘
pid                                     
st                    └────────────────────┘
667  | (a::l) hl :=
id      └┘  └┘
src      └┘
typ     └┘  └┘
668  have hl' : l.nodup, from nodup_of_nodup_cons hl,
id               └────┘       └─────────────────┘
src              └────┘       └─────────────────┘
typ              └────┘       └─────────────────┘
doc              └────┘
669  have hln' : (perms_of_list l).nodup, from nodup_perms_of_list hl',
id                └───────────┘   └───┘        └─────────────────┘ └─┘
src               └───────────┘   └───┘
typ               └───────────┘   └───┘        └─────────────────┘ └─┘
doc                               └───┘
670  have hmeml : ∀ {f : perm α}, f ∈ perms_of_list l → f a = a,
id                       └──┘      └───────────┘        
src                      └──┘        └───────────┘         
typ                      └──┘      └───────────┘        
doc                      └──┘
671    from λ f hf, not_not.1 (mt (mem_of_mem_perms_of_list hf) (nodup_cons.1 hl).1),
id             └┘  └─────┘   └┘  └──────────────────────┘ └┘   └────────┘     
src                 └─────┘   └┘  └──────────────────────┘      └────────┘     
typ            └┘  └─────┘   └┘  └──────────────────────┘ └┘   └────────┘     
672  by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le]; exact
id          └───────────┘  └───────────────┘  └─────────────┘  └─────────────────┘
src     └──┘└───────────┘└┘└───────────────┘└┘└─────────────┘└┘└─────────────────┘  └────┘
typ     └──┘└───────────┘└┘└───────────────┘└┘└─────────────┘└┘└─────────────────┘  └────┘
doc     └──┘             └┘                 └┘               └┘                     └────┘
txt     └──┘             └┘                 └┘               └┘                     └────┘
par     └──┘             └┘                 └┘               └┘                     └────┘
pid       └┘             └┘                 └┘               └┘                          
st     └────────────────┘└─────────────────┘└───────────────┘└───────────────────┘└───────
673  ⟨hln', ⟨λ _ _, nodup_map (λ _ _, (mul_left_inj _).1) hln',
id                  └───────┘          └──────────┘       └──┘
src       └┘  └────┘└───────┘  └────┘ └──────────┘└─────┘    └─
typ       └┘  └────┘└───────┘  └────┘ └──────────┘└─────┘└──┘└─
doc       └┘  └────┘           └────┘             └─────┘    └─
txt       └┘  └────┘           └────┘             └─────┘    └─
par       └┘  └────┘           └────┘             └─────┘    └─
pid       └┘  └────┘           └────┘             └─────┘    └─
st   ───────────────────────────────────────────────────────────
674    λ i j hj hij x hx₁ hx₂,
src  ─┘ └──────────────────────
typ  ─┘ └──────────────────────
doc  ─┘ └──────────────────────
txt  ─┘ └──────────────────────
par  ─┘ └──────────────────────
pid  ─┘ └──────────────────────
st   ──────────────────────────
675      let ⟨f, hf⟩ := list.mem_map.1 hx₁ in
id               └┘
src  ───┘     └┘  └───┘            └─┘   └───
typ  ───┘     └┘└┘└───┘            └─┘   └───
doc  ───┘     └┘  └───┘            └─┘   └───
txt  ───┘     └┘  └───┘            └─┘   └───
par  ───┘     └┘  └───┘            └─┘   └───
pid  ───┘     └┘  └───┘            └─┘   └───
st   ─────────────────────────────────────────
676      let ⟨g, hg⟩ := list.mem_map.1 hx₂ in
id               └┘
src  ───┘     └┘  └───┘            └─┘   └───
typ  ───┘     └┘└┘└───┘            └─┘   └───
doc  ───┘     └┘  └───┘            └─┘   └───
txt  ───┘     └┘  └───┘            └─┘   └───
par  ───┘     └┘  └───┘            └─┘   └───
pid  ───┘     └┘  └───┘            └─┘   └───
st   ─────────────────────────────────────────
677      have hix : x a = nth_le l i (lt_trans hij hj),
id                                               └┘
src  ───┘    └─────┘                        └──
typ  ───┘    └─────┘                     └┘└──
doc  ───┘    └─────┘                         └──
txt  ───┘    └─────┘                         └──
par  ───┘    └─────┘                         └──
pid  ───┘    └─────┘                         └──
st   ───────────────────────────────────────────────────
678        by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left],
id                  └┘    └───────┘  └───┘ └┘    └─────────────┘
src  ────────┘└────┘  └──┘└───────┘└┘       └──┘└─────────────┘└─
typ  ────────┘└────┘└┘└──┘└───────┘└┘└───┘└┘└──┘└─────────────┘└─
doc  ────────┘└────┘  └──┘         └┘       └──┘               └─
txt  ────────┘└────┘  └──┘         └┘       └──┘               └─
par  ────────┘└────┘  └──┘         └┘       └──┘               └─
pid  ──────────────┘  └──┘         └┘       └──┘               └──
st   ───────┘└───────┘└───────────┘└────────┘└─────────────────┘└─
679      have hiy : x a = nth_le l j hj,
id                        └────┘    └┘
src  ───┘    └─────┘   └────┘    └─
typ  ───┘    └─────┘   └────┘ └┘└─
doc  ───┘    └─────┘             └─
txt  ───┘    └─────┘             └─
par  ───┘    └─────┘             └─
pid  ───┘    └─────┘             └─
st   ────────────────────────────────────
680        by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left],
id                  └┘    └───────┘  └───┘ └┘    └─────────────┘
src  ────────┘└────┘  └──┘└───────┘└┘       └──┘└─────────────┘└─
typ  ────────┘└────┘└┘└──┘└───────┘└┘└───┘└┘└──┘└─────────────┘└─
doc  ────────┘└────┘  └──┘         └┘       └──┘               └─
txt  ────────┘└────┘  └──┘         └┘       └──┘               └─
par  ────────┘└────┘  └──┘         └┘       └──┘               └─
pid  ──────────────┘  └──┘         └┘       └──┘               └──
st   ───────┘└───────┘└───────────┘└────────┘└─────────────────┘└─
681      absurd (hf.2.trans (hg.2.symm)) $
id       └────┘
src  ───┘└────┘   └───────┘   └────────┘ 
typ  ───┘└────┘   └───────┘   └────────┘ 
doc  ───┘         └───────┘   └────────┘ 
txt  ───┘         └───────┘   └────────┘ 
par  ───┘         └───────┘   └────────┘ 
pid  ───┘         └───────┘   └────────┘ 
st   ──────────────────────────────────────
682        λ h, ne_of_lt hij $ nodup_iff_nth_le_inj.1 hl' i j (lt_trans hij hj) hj $
id              └──────┘       └──────────────────┘   └─┘    └──────┘     └┘
src  ─────┘ └──┘└──────┘    └──────────────────┘└─┘      └──────┘     └┘   
typ  ─────┘ └──┘└──────┘    └──────────────────┘└─┘└─┘ └──────┘   └┘└┘   
doc  ─────┘ └──┘                                └─┘                   └┘   
txt  ─────┘ └──┘                                └─┘                   └┘   
par  ─────┘ └──┘                                └─┘                   └┘   
pid  ─────┘ └──┘                                └─┘                   └┘   
st   ────────────────────────────────────────────────────────────────────────────────
683          by rw [← hix, hiy]⟩,
id                    └─┘  └─┘
src  ───────┘  └────┘   └┘   └──
typ  ───────┘  └────┘└─┘└┘└─┘└──
doc  ───────┘  └────┘   └┘   └──
txt  ───────┘  └────┘   └┘   └──
par  ───────┘  └────┘   └┘   └──
pid  ───────┘  └─────┘   └┘   └───
st   ─────────┘└────────┘└───┘└──
684    λ f hf₁ hf₂,
src  ─┘ └───────────
typ  ─┘ └───────────
doc  ─┘ └───────────
txt  ─┘ └───────────
par  ─┘ └───────────
pid  ─┘ └───────────
st   ───────────────
685      let ⟨x, hx, hx'⟩ := list.mem_bind.1 hf₂ in
id              └┘  └─┘     └───────────┘
src  ───┘     └┘  └┘   └───┘└───────────┘└─┘   └───
typ  ───┘    └┘└┘└┘└─┘└───┘└───────────┘└─┘   └───
doc  ───┘     └┘  └┘   └───┘             └─┘   └───
txt  ───┘     └┘  └┘   └───┘             └─┘   └───
par  ───┘     └┘  └┘   └───┘             └─┘   └───
pid  ───┘     └┘  └┘   └───┘             └─┘   └───
st   ───────────────────────────────────────────────
686      let ⟨g, hg⟩ := list.mem_map.1 hx' in
id              └┘     └──────────┘
src  ───┘     └┘  └───┘└──────────┘└─┘   └───
typ  ───┘    └┘└┘└───┘└──────────┘└─┘   └───
doc  ───┘     └┘  └───┘            └─┘   └───
txt  ───┘     └┘  └───┘            └─┘   └───
par  ───┘     └┘  └───┘            └─┘   └───
pid  ───┘     └┘  └───┘            └─┘   └───
st   ─────────────────────────────────────────
687      have hgxa : g⁻¹ x = a, from f.injective $
id                    └┘              └────────┘
src  ───┘    └──────┘ └┘   └─────┘ └────────┘ 
typ  ───┘    └──────┘ └┘   └─────┘ └────────┘ 
doc  ───┘    └──────┘      └─────┘            
txt  ───┘    └──────┘      └─────┘            
par  ───┘    └──────┘      └─────┘            
pid  ───┘    └──────┘      └─────┘            
st   ──────────────────────────────────────────────
688        by rw [hmeml hf₁, ← hg.2]; simp,
id                └───┘ └─┘    └┘
src  ─────┘  └──┘        └──┘  └─┘└┘└──┘└─
typ  ─────┘  └──┘└───┘└─┘└──┘└┘└─┘└┘└──┘└─
doc  ─────┘  └──┘        └──┘  └─┘└┘└──┘└─
txt  ─────┘  └──┘        └──┘  └─┘└┘└──┘└─
par  ─────┘  └──┘        └──┘  └─┘└┘└──┘└─
pid  ─────┘  └───┘        └──┘  └──────────
st   ───────┘└────────────┘└────┘└─┘└────┘└─
689      have hxa : x ≠ a, from λ h, (list.nodup_cons.1 hl).1 (h ▸ hx),
id                                  └─────────────┘   └┘
src  ───┘    └─────┘  └─────┘ └──┘ └─────────────┘└─┘  └──┘     └──
typ  ───┘    └─────┘ └─────┘ └──┘ └─────────────┘└─┘└┘└──┘     └──
doc  ───┘    └─────┘   └─────┘ └──┘                └─┘  └──┘     └──
txt  ───┘    └─────┘   └─────┘ └──┘                └─┘  └──┘     └──
par  ───┘    └─────┘   └─────┘ └──┘                └─┘  └──┘     └──
pid  ───┘    └─────┘   └─────┘ └──┘                └─┘  └──┘     └──
st   ───────────────────────────────────────────────────────────────────
690      (list.nodup_cons.1 hl).1 $
src  ───┘                └─┘  └──┘ 
typ  ───┘                └─┘  └──┘ 
doc  ───┘                └─┘  └──┘ 
txt  ───┘                └─┘  └──┘ 
par  ───┘                └─┘  └──┘ 
pid  ───┘                └─┘  └──┘ 
st   ───────────────────────────────
691        hgxa ▸ mem_of_mem_perms_of_list hg.1 (by rwa [apply_inv_self, hgxa])⟩
id               └──────────────────────┘               └────────────┘  └──┘
src  ─────┘    └──────────────────────┘  └─┘   └───┘└────────────┘└┘    └──
typ  ─────┘    └──────────────────────┘  └─┘   └───┘└────────────┘└┘└──┘└──
doc  ─────┘                               └─┘   └───┘              └┘    └──
txt  ─────┘                               └─┘   └───┘              └┘    └──
par  ─────┘                               └─┘   └───┘              └┘    └──
pid  ─────┘                               └─┘   └────┘              └┘    └─┘
st   ─────────────────────────────────────────────┘└──────────────────┘└────┘└──
692  
src  
typ  
doc  
txt  
par  
pid  
st   
693  def perms_of_finset (s : finset α) : finset (perm α) :=
id                            └────┘     └────┘  └──┘ 
src                           └────┘      └────┘  └──┘
typ                           └────┘     └────┘  └──┘ 
doc                           └────┘      └────┘  └──┘
694  quotient.hrec_on s.1 (λ l hl, ⟨perms_of_list l, nodup_perms_of_list hl⟩)
id   └──────────────┘       └┘   └───────────┘   └─────────────────┘ └┘
src  └──────────────┘              └───────────┘    └─────────────────┘
typ  └──────────────┘       └┘   └───────────┘   └─────────────────┘ └┘
695    (λ a b hab, hfunext (congr_arg _ (quotient.sound hab))
id          └─┘  └─────┘  └───────┘    └────────────┘ └─┘
src                └─────┘  └───────┘    └────────────┘
typ         └─┘  └─────┘  └───────┘    └────────────┘ └─┘
696      (λ ha hb _, heq_of_eq $ finset.ext.2 $
id          └┘ └┘   └───────┘   └────────┘
src                  └───────┘   └────────┘
typ         └┘ └┘   └───────┘   └────────┘
697        by simp [mem_perms_of_list_iff,mem_of_perm hab]))
id                  └───────────────────┘ └─────────┘ └─┘
src           └────┘└───────────────────┘└─────────┘   
typ           └────┘└───────────────────┘└─────────┘└─┘
doc           └────┘                                   
txt           └────┘                                   
par           └────┘                                   
pid                                                  
st           └───────────────────────────────────────────┘
698    s.2
id     
src     
typ    
699  
700  lemma mem_perms_of_finset_iff : ∀ {s : finset α} {f : perm α},
id                                          └────┘        └──┘ 
src                                         └────┘         └──┘
typ                                         └────┘        └──┘ 
doc                                         └────┘         └──┘
701    f ∈ perms_of_finset s ↔ ∀ {x}, f x ≠ x → x ∈ s :=
id       └─────────────┘                 
src       └─────────────┘                      
typ      └─────────────┘                 
702  by rintros ⟨⟨l⟩, hs⟩ f; exact mem_perms_of_list_iff
id                                 └───────────────────┘
src     └─────────────────┘  └────┘└───────────────────┘
typ     └─────────────────┘  └────┘└───────────────────┘
doc     └─────────────────┘  └────┘                     
txt     └─────────────────┘  └────┘                     
par     └─────────────────┘  └────┘                     
pid            └──────────┘                            
st     └─────────────────────────────────────────────────
703  
src  
typ  
doc  
txt  
par  
pid  
st   
704  lemma card_perms_of_finset : ∀ (s : finset α),
id                                       └────┘ 
src                                      └────┘
typ                                      └────┘ 
doc                                      └────┘
705    (perms_of_finset s).card = s.card.fact :=
id      └─────────────┘  └──┘   └───┘└───┘
src     └─────────────┘   └──┘    └───┘└───┘
typ     └─────────────┘  └──┘   └───┘└───┘
doc                       └──┘     └───┘└───┘
706  by rintros ⟨⟨l⟩, hs⟩; exact length_perms_of_list l
id                               └──────────────────┘ 
src     └───────────────┘  └────┘└──────────────────┘ 
typ     └───────────────┘  └────┘└──────────────────┘
doc     └───────────────┘  └────┘                     
txt     └───────────────┘  └────┘                     
par     └───────────────┘  └────┘                     
pid            └────────┘                            
st     └────────────────────────────────────────────────
707  
src  
typ  
doc  
txt  
par  
pid  
st   
708  def fintype_perm [fintype α] : fintype (perm α) :=
id                     └─────┘     └─────┘  └──┘ 
src                    └─────┘      └─────┘  └──┘
typ                    └─────┘     └─────┘  └──┘ 
doc                    └─────┘      └─────┘  └──┘
709  ⟨perms_of_finset (@finset.univ α _), by simp [mem_perms_of_finset_iff]⟩
id    └─────────────┘   └─────────┘               └─────────────────────┘
src   └─────────────┘   └─────────┘          └────┘└─────────────────────┘
typ   └─────────────┘   └─────────┘         └────┘└─────────────────────┘
doc                     └─────────┘          └────┘                       
txt                                          └────┘                       
par                                          └────┘                       
pid                                                                     
st                                          └─────────────────────────────┘
710  
711  instance [fintype α] [fintype β] : fintype (α ≃ β) :=
id             └─────┘    └─────┘     └─────┘    
src            └─────┘     └─────┘      └─────┘    
typ            └─────┘    └─────┘     └─────┘    
doc            └─────┘     └─────┘      └─────┘    
712  if h : fintype.card β = fintype.card α
id   └┘     └──────────┘   └──────────┘ 
src  └┘     └──────────┘    └──────────┘
typ  └┘     └──────────┘   └──────────┘ 
doc         └──────────┘     └──────────┘
713  then trunc.rec_on_subsingleton (fintype.equiv_fin α)
id        └───────────────────────┘  └───────────────┘ 
src       └───────────────────────┘  └───────────────┘
typ       └───────────────────────┘  └───────────────┘ 
doc                                  └───────────────┘
714    (λ eα, trunc.rec_on_subsingleton (fintype.equiv_fin β)
id        └┘  └───────────────────────┘  └───────────────┘ 
src           └───────────────────────┘  └───────────────┘
typ       └┘  └───────────────────────┘  └───────────────┘ 
doc                                      └───────────────┘
715      (λ eβ, @fintype.of_equiv _ (perm α) fintype_perm
id          └┘   └──────────────┘    └──┘   └──────────┘
src              └──────────────┘    └──┘    └──────────┘
typ         └┘   └──────────────┘    └──┘   └──────────┘
doc              └──────────────┘    └──┘
716        (equiv_congr (equiv.refl α) (eα.trans (eq.rec_on h eβ.symm)) : (α ≃ α) ≃ (α ≃ β))))
id          └─────────┘  └────────┘    └┘└────┘  └───────┘  └┘└───┘              
src         └─────────┘  └────────┘       └────┘  └───────┘     └───┘                
typ         └─────────┘  └────────┘    └┘└────┘  └───────┘  └┘└───┘              
doc                                                                                  
717  else ⟨∅, λ x, false.elim (h (fintype.card_eq.2 ⟨x.symm⟩))⟩
id              └────────┘    └─────────────┘   └───┘
src               └────────┘     └─────────────┘    └───┘
typ             └────────┘    └─────────────┘   └───┘
718  
719  lemma fintype.card_perm [fintype α] : fintype.card (perm α) = (fintype.card α).fact :=
id                            └─────┘     └──────────┘  └──┘     └──────────┘  └──┘
src                           └─────┘      └──────────┘  └──┘      └──────────┘   └──┘
typ                           └─────┘     └──────────┘  └──┘     └──────────┘  └──┘
doc                           └─────┘      └──────────┘  └──┘       └──────────┘   └──┘
720  subsingleton.elim (@fintype_perm α _ _) (@equiv.fintype α α _ _ _ _) ▸
id   └───────────────┘   └──────────┘         └───────────┘            
src  └───────────────┘   └──────────┘          └───────────┘              
typ  └───────────────┘   └──────────┘         └───────────┘            
721  card_perms_of_finset _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
722  
723  lemma fintype.card_equiv [fintype α] [fintype β] (e : α ≃ β) :
id                             └─────┘    └─────┘          
src                            └─────┘     └─────┘           
typ                            └─────┘    └─────┘          
doc                            └─────┘     └─────┘           
724    fintype.card (α ≃ β) = (fintype.card α).fact :=
id     └──────────┘        └──────────┘  └──┘
src    └──────────┘          └──────────┘   └──┘
typ    └──────────┘        └──────────┘  └──┘
doc    └──────────┘           └──────────┘   └──┘
725  fintype.card_congr (equiv_congr (equiv.refl α) e) ▸ fintype.card_perm
id   └────────────────┘  └─────────┘  └────────┘      └───────────────┘
src  └────────────────┘  └─────────┘  └────────┘        └───────────────┘
typ  └────────────────┘  └─────────┘  └────────┘      └───────────────┘
726  
727  end equiv
728  
729  namespace fintype
730  
731  section choose
732  open fintype
733  open equiv
734  
735  variables [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p]
id              └─────┘     └──────────┘                    └────────────┘
src             └─────┘     └──────────┘                    └────────────┘
typ             └─────┘     └──────────┘                    └────────────┘
doc             └─────┘
736  
737  def choose_x (hp : ∃! a : α, p a) : {a // p a} :=
id                      └┘                
src                     └┘              
typ                     └┘                
738  ⟨finset.choose p univ (by simp; exact hp), finset.choose_property _ _ _⟩
id    └───────────┘  └──┘                 └┘   └────────────────────┘
src   └───────────┘   └──┘     └──┘  └────┘     └────────────────────┘
typ   └───────────┘  └──┘     └──┘  └────┘└┘   └────────────────────┘
doc                   └──┘     └──┘  └────┘
txt                            └──┘  └────┘
par                            └──┘  └────┘
pid                                       
st                            └─────────────┘
739  
740  def choose (hp : ∃! a, p a) : α := choose_x p hp
id                    └┘           └──────┘  └┘
src                   └┘               └──────┘
typ                   └┘           └──────┘  └┘
st                             
741  
742  lemma choose_spec (hp : ∃! a, p a) : p (choose p hp) :=
id                           └┘         └────┘  └┘
src                          └┘             └────┘
typ                          └┘         └────┘  └┘
743  (choose_x p hp).property
id    └──────┘  └┘ └──────┘
src   └──────┘      └──────┘
typ   └──────┘  └┘ └──────┘
744  
745  end choose
746  
747  section bijection_inverse
748  open function
749  
750  variables [fintype α] [decidable_eq α]
id              └─────┘     └──────────┘
src             └─────┘     └──────────┘
typ             └─────┘     └──────────┘
doc             └─────┘
751  variables [fintype β] [decidable_eq β]
id              └─────┘     └──────────┘
src             └─────┘     └──────────┘
typ             └─────┘     └──────────┘
doc             └─────┘
752  variables {f : α → β}
753  
754  /-- `
755  `bij_inv f` is the unique inverse to a bijection `f`. This acts
756    as a computable alternative to `function.inv_fun`. -/
757  def bij_inv (f_bij : bijective f) (b : β) : α :=
id                        └───────┘            
src                       └───────┘
typ                       └───────┘            
758  fintype.choose (λ a, f a = b)
id   └────────────┘         
src  └────────────┘           
typ  └────────────┘         
759  begin
st   └─────
760    rcases f_bij.right b with ⟨a', fa_eq_b⟩,
id            └─────────┘ 
src    └─────┘└─────────┘ └─────────────────┘
typ    └─────┘└─────────┘└─────────────────┘
doc    └─────┘            └─────────────────┘
txt    └─────┘            └─────────────────┘
par    └─────┘            └─────────────────┘
pid                      └─────────────────┘
st   ────────────────────────────────────────┘└─
761    rw ← fa_eq_b,
id          └─────┘
src    └───┘
typ    └───┘└─────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ─────────────┘└─
762    exact ⟨a', ⟨rfl, (λ a h, f_bij.left h)⟩⟩
id            └┘   └─┘          └────────┘
src    └────┘   └┘ └─┘└┘  └────┘└────────┘ └──┘
typ    └────┘ └┘└┘ └─┘└┘  └────┘└────────┘ └──┘
doc    └────┘   └┘    └┘  └────┘           └──┘
txt    └────┘   └┘    └┘  └────┘           └──┘
par    └────┘   └┘    └┘  └────┘           └──┘
pid            └┘    └┘  └────┘           └─┘
st   ──────────────────────────────────────────┘
763  end
st   └─┘
764  
765  lemma left_inverse_bij_inv (f_bij : bijective f) : left_inverse (bij_inv f_bij) f :=
id                                       └───────┘     └──────────┘  └─────┘ └───┘  
src                                      └───────┘      └──────────┘  └─────┘
typ                                      └───────┘     └──────────┘  └─────┘ └───┘  
doc                                                                   └─────┘
766  λ a, f_bij.left (choose_spec (λ a', f a' = f a) _)
id       └───┘└───┘  └─────────┘    └┘   └┘   
src            └───┘  └─────────┘             
typ      └───┘└───┘  └─────────┘    └┘   └┘   
767  
768  lemma right_inverse_bij_inv (f_bij : bijective f) : right_inverse (bij_inv f_bij) f :=
id                                        └───────┘     └───────────┘  └─────┘ └───┘  
src                                       └───────┘      └───────────┘  └─────┘
typ                                       └───────┘     └───────────┘  └─────┘ └───┘  
doc                                                                     └─────┘
769  λ b, choose_spec (λ a', f a' = b) _
id       └─────────┘    └┘   └┘  
src       └─────────┘             
typ      └─────────┘    └┘   └┘  
770  
771  lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
id                                    └───────┘     └───────┘  └─────┘ └───┘
src                                   └───────┘      └───────┘  └─────┘
typ                                   └───────┘     └───────┘  └─────┘ └───┘
doc                                                             └─────┘
772  ⟨injective_of_left_inverse (right_inverse_bij_inv _),
id    └───────────────────────┘  └───────────────────┘
src   └───────────────────────┘  └───────────────────┘
typ   └───────────────────────┘  └───────────────────┘
773      surjective_of_has_right_inverse ⟨f, left_inverse_bij_inv _⟩⟩
id       └─────────────────────────────┘    └──────────────────┘
src      └─────────────────────────────┘     └──────────────────┘
typ      └─────────────────────────────┘    └──────────────────┘
774  
775  end bijection_inverse
776  
777  lemma well_founded_of_trans_of_irrefl [fintype α] (r : α → α → Prop)
id                                          └─────┘           
src                                         └─────┘
typ                                         └─────┘           
doc                                         └─────┘
778    [is_trans α r] [is_irrefl α r] : well_founded r :=
id      └──────┘     └───────┘      └──────────┘ 
src     └──────┘       └───────┘        └──────────┘
typ     └──────┘     └───────┘      └──────────┘ 
779  by classical; exact
src     └───────┘  └────┘
typ     └───────┘  └────┘
doc     └───────┘  └────┘
txt     └───────┘  └────┘
par     └───────┘  └────┘
pid                     
st     └─────────────────
780  have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r z y)).card,
id                                                        └─────────┘       
src       └──┘                   └──┘   └──────┘ └─────────┘  └──┘   └────────
typ       └──┘                  └──┘   └──────┘ └─────────┘  └──┘  └────────
doc       └──┘                   └──┘   └──────┘  └─────────┘  └──┘   └────────
txt       └──┘                   └──┘   └──────┘               └──┘   └────────
par       └──┘                   └──┘   └──────┘               └──┘   └────────
pid       └──┘                   └──┘   └──────┘               └──┘   └────────
st   ───────────────────────────────────────────────────────────────────────────────────────
781    from λ x y hxy, finset.card_lt_card $
id                     └─────────────────┘
src  ──────┘ └────────┘└─────────────────┘ 
typ  ──────┘ └────────┘└─────────────────┘ 
doc  ──────┘ └────────┘                    
txt  ──────┘ └────────┘                    
par  ──────┘ └────────┘                    
pid  ──────┘ └────────┘                    
st   ────────────────────────────────────────
782      by simp only [finset.lt_iff_ssubset.symm, lt_iff_le_not_le,
id                                                 └──────────────┘
src  ───┘  └─────────┘                          └┘└──────────────┘└─
typ  ───┘  └─────────┘└────────────────────────┘└┘└──────────────┘└─
doc  ───┘  └─────────┘                          └┘                └─
txt  ───┘  └─────────┘                          └┘                └─
par  ───┘  └─────────┘                          └┘                └─
pid  ───┘  └──────────┘                          └┘                └─
st   ─────┘└─────────────────────────────────────────────────────────
783        finset.le_iff_subset, finset.subset_iff, mem_filter, true_and, mem_univ, hxy];
id         └──────────────────┘  └───────────────┘  └────────┘  └──────┘  └──────┘  └─┘
src  ─────┘└──────────────────┘└┘└───────────────┘└┘└────────┘└┘└──────┘└┘└──────┘└┘   └─
typ  ─────┘└──────────────────┘└┘└───────────────┘└┘└────────┘└┘└──────┘└┘└──────┘└┘└─┘└─
doc  ─────┘                    └┘                 └┘          └┘        └┘        └┘   └─
txt  ─────┘                    └┘                 └┘          └┘        └┘        └┘   └─
par  ─────┘                    └┘                 └┘          └┘        └┘        └┘   └─
pid  ─────┘                    └┘                 └┘          └┘        └┘        └┘   └──
st   ─────────────────────────────────────────────────────────────────────────────────────
784      exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩,
id                       └───┘          └──────────────────────┘     └─────┘    └─┘  └────┘ 
src  ─────────┘  └──────┘└───┘      └┘└──────────────────────┘  └┘└─────┘└─┘    └┘└────┘ └───┘
typ  ─────────┘  └──────┘└───┘      └┘└──────────────────────┘  └┘└─────┘└─┘ └─┘└┘└────┘└───┘
doc  ─────────┘  └──────┘           └┘                          └┘       └─┘    └┘       └───┘
txt  ─────────┘  └──────┘           └┘                          └┘       └─┘    └┘       └───┘
par  ─────────┘  └──────┘           └┘                          └┘       └─┘    └┘       └───┘
pid  ─────────┘  └──────┘           └┘                          └┘       └─┘    └┘       └───┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
785  subrelation.wf this (measure_wf _)
id   └────────────┘       └────────┘
src  └────────────┘     └────────┘└───
typ  └────────────┘     └────────┘└───
doc                               └───
txt                               └───
par                               └───
pid                               └─┘
st   ───────────────────────────────────
786  
src  
typ  
doc  
txt  
par  
pid  
st   
787  lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
id                                └─────┘    └──────┘     └──────────┘          
src                               └─────┘     └──────┘      └──────────┘  
typ                               └─────┘    └──────┘     └──────────┘          
doc                               └─────┘
788  well_founded_of_trans_of_irrefl _
id   └─────────────────────────────┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘
789  
790  @[instance, priority 10] lemma linear_order.is_well_order [fintype α] [linear_order α] :
id                                                              └─────┘    └──────────┘ 
src                                                             └─────┘     └──────────┘
typ                                                             └─────┘    └──────────┘ 
doc                                                             └─────┘
791    is_well_order α (<) :=
id     └───────────┘  
src    └───────────┘   
typ    └───────────┘  
doc    └───────────┘
792  { wf := preorder.well_founded }
id           └───────────────────┘
src          └───────────────────┘
typ          └───────────────────┘
793  
794  end fintype
795  
796  class infinite (α : Type*) : Prop :=
id                       └───┘
typ                      └───┘
797  (not_fintype : fintype α → false)
id                  └─────┘   └───┘
src                 └─────┘     └───┘
typ                 └─────┘   └───┘
doc                 └─────┘
798  
799  @[simp] lemma not_nonempty_fintype {α : Type*} : ¬nonempty (fintype α) ↔ infinite α :=
id                                                    └──────┘  └─────┘    └──────┘ 
src                                                   └──────┘  └─────┘     └──────┘
typ                                                   └──────┘  └─────┘    └──────┘ 
doc    └──┘                                                      └─────┘
800  ⟨λf, ⟨λ x, f ⟨x⟩⟩, λ⟨f⟩ ⟨x⟩, f x⟩
id                     
typ                    
801  
802  namespace infinite
803  
804  lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
id                                └──────┘        └────┘         
src                               └──────┘         └────┘           
typ                               └──────┘        └────┘         
doc                                                └────┘
805  classical.not_forall.1 $ λ h, not_fintype ⟨s, h⟩
id   └──────────────────┘        └─────────┘    
src  └──────────────────┘         └─────────┘
typ  └──────────────────┘        └─────────┘    
806  
807  @[priority 100] -- see Note [lower instance priority]
808  instance nonempty (α : Type*) [infinite α] : nonempty α :=
id                                  └──────┘     └──────┘ 
src                                 └──────┘      └──────┘
typ                                 └──────┘     └──────┘ 
809  nonempty_of_exists (exists_not_mem_finset (∅ : finset α))
id   └────────────────┘  └───────────────────┘     └────┘ 
src  └────────────────┘  └───────────────────┘     └────┘
typ  └────────────────┘  └───────────────────┘     └────┘ 
doc                                                 └────┘
810  
811  lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite α :=
id                       └──────┘                   └───────┘     └──────┘ 
src                      └──────┘                      └───────┘      └──────┘
typ                      └──────┘                   └───────┘     └──────┘ 
812  ⟨λ I, by exactI not_fintype (fintype.of_injective f hf)⟩
id                  └─────────┘  └──────────────────┘  └┘
src           └─────┘└─────────┘ └──────────────────┘   
typ          └─────┘└─────────┘ └──────────────────┘└┘
doc           └─────┘                                   
txt           └─────┘                                   
par           └─────┘                                   
pid                                                    
st           └─────────────────────────────────────────────┘
813  
814  lemma of_surjective [infinite β] (f : α → β) (hf : surjective f) : infinite α :=
id                        └──────┘                   └────────┘     └──────┘ 
src                       └──────┘                      └────────┘      └──────┘
typ                       └──────┘                   └────────┘     └──────┘ 
815  ⟨λ I, by classical; exactI not_fintype (fintype.of_surjective f hf)⟩
id                             └─────────┘  └───────────────────┘  └┘
src           └───────┘  └─────┘└─────────┘ └───────────────────┘   
typ          └───────┘  └─────┘└─────────┘ └───────────────────┘└┘
doc           └───────┘  └─────┘            └───────────────────┘   
txt           └───────┘  └─────┘                                    
par           └───────┘  └─────┘                                    
pid                                                                
st           └─────────────────────────────────────────────────────────┘
816  
817  private noncomputable def nat_embedding_aux (α : Type*) [infinite α] : ℕ → α
id                                                            └──────┘       
src                                                           └──────┘      
typ                                                           └──────┘       
818  | n := by letI := classical.dec_eq α; exact classical.some (exists_not_mem_finset
id                     └──────────────┘         └────────────┘  └───────────────────┘
src            └──────┘└──────────────┘   └────┘└────────────┘ └───────────────────┘
typ            └──────┘└──────────────┘  └────┘└────────────┘ └───────────────────┘
doc            └──────┘                   └────┘                                    
txt            └──────┘                   └────┘                                    
par            └──────┘                   └────┘                                    
pid                └─┘                                                            
st            └────────────────────────────────────────────────────────────────────────
819    ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux m)
id       └────────────┘                          └───────────────┘
src  ─┘  └────────────┘ └─────┘  └───────┘  └─┘                  └─
typ  ─┘  └────────────┘ └─────┘  └───────┘ └─┘└───────────────┘ └─
doc  ─┘  └────────────┘ └─────┘  └───────┘   └─┘                  └─
txt  ─┘                 └─────┘  └───────┘   └─┘                  └─
par  ─┘                 └─────┘  └───────┘   └─┘                  └─
pid  ─┘                 └─────┘  └───────┘   └─┘                  └─
st   ───────────────────────────────────────────────────────────────────
820      (λ _, multiset.mem_range.1)).to_finset)
id             └────────────────┘
src  ───┘  └──┘└────────────────┘└───────────────
typ  ───┘  └──┘└────────────────┘└───────────────
doc  ───┘  └──┘                  └───────────────
txt  ───┘  └──┘                  └───────────────
par  ───┘  └──┘                  └───────────────
pid  ───┘  └──┘                  └─────────────┘
st   ────────────────────────────────────────────
821  
src  
typ  
doc  
txt  
par  
pid  
st   
822  private lemma nat_embedding_aux_injective (α : Type*) [infinite α] :
id                                                          └──────┘ 
src                                                         └──────┘
typ                                                         └──────┘ 
823    function.injective (nat_embedding_aux α) :=
id     └────────────────┘  └───────────────┘ 
src    └────────────────┘  └───────────────┘
typ    └────────────────┘  └───────────────┘ 
824  begin
st   └─────
825    assume m n h,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid    └──────────┘
st   ─────────────┘└─
826    letI := classical.dec_eq α,
id             └──────────────┘ 
src    └──────┘└──────────────┘
typ    └──────┘└──────────────┘
doc    └──────┘                
txt    └──────┘                
par    └──────┘                
pid        └─┘                
st   ───────────────────────────┘└─
827    wlog hmlen : m ≤ n using m n,
id                    
src    └───────────┘  └────────┘
typ    └───────────┘└────────┘
doc    └───────────┘   └────────┘
txt    └───────────┘   └────────┘
par    └───────────┘   └────────┘
pid        └────┘└─┘   └───────┘
st   ─────────────────────────────┘└─
828    by_contradiction hmn,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid                    └──┘
st   ─────────────────────┘└─
829    have hmn : m < n, from lt_of_le_of_ne hmlen hmn,
id                         └────────────┘ └───┘ └─┘
src    └─────────┘    └───┘└────────────┘     
typ    └─────────┘  └───┘└────────────┘└───┘└─┘
doc    └─────────┘     └───┘                   
txt    └─────────┘     └───┘                   
par    └─────────┘     └───┘                   
pid    └──────┘└─┘     └───┘                   
st   ─────────────────┘└─────────────────────────────┘└─
830    refine (classical.some_spec (exists_not_mem_finset
id             └─────────────────┘  └───────────────────┘
src    └─────┘ └─────────────────┘ └───────────────────┘
typ    └─────┘ └─────────────────┘ └───────────────────┘
doc    └─────┘                                          
txt    └─────┘                                          
par    └─────┘                                          
pid                                                    
st   ─────────────────────────────────────────────────────
831      ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux α m)
id         └────────────┘                          └───────────────┘ 
src  ───┘  └────────────┘ └─────┘  └───────┘   └─┘└───────────────┘  └─
typ  ───┘  └────────────┘ └─────┘  └───────┘ └─┘└───────────────┘ └─
doc  ───┘  └────────────┘ └─────┘  └───────┘   └─┘                   └─
txt  ───┘                 └─────┘  └───────┘   └─┘                   └─
par  ───┘                 └─────┘  └───────┘   └─┘                   └─
pid  ───┘                 └─────┘  └───────┘   └─┘                   └─
st   ───────────────────────────────────────────────────────────────────────
832        (λ _, multiset.mem_range.1)).to_finset)) _,
id               └────────────────┘
src  ─────┘  └──┘└────────────────┘└────────────────┘
typ  ─────┘  └──┘└────────────────┘└────────────────┘
doc  ─────┘  └──┘                  └────────────────┘
txt  ─────┘  └──┘                  └────────────────┘
par  ─────┘  └──┘                  └────────────────┘
pid  ─────┘  └──┘                  └────────────────┘
st   ───────────────────────────────────────────────┘└─
833    refine multiset.mem_to_finset.2 (multiset.mem_pmap.2
id            └────────────────────┘    └───────────────┘
src    └─────┘└────────────────────┘└─┘ └───────────────┘└──
typ    └─────┘└────────────────────┘└─┘ └───────────────┘└──
doc    └─────┘                      └─┘                  └──
txt    └─────┘                      └─┘                  └──
par    └─────┘                      └─┘                  └──
pid                                └─┘                  └──
st   ───────────────────────────────────────────────────────
834      ⟨m, multiset.mem_range.2 hmn, _⟩),
id          └────────────────┘   └─┘
src  ───┘  └┘└────────────────┘└─┘   └───┘
typ  ───┘ └┘└────────────────┘└─┘└─┘└───┘
doc  ───┘  └┘                  └─┘   └───┘
txt  ───┘  └┘                  └─┘   └───┘
par  ───┘  └┘                  └─┘   └───┘
pid  ───┘  └┘                  └─┘   └───┘
st   ────────────────────────────────────┘└─
835    rw [h, nat_embedding_aux]
id           └───────────────┘
src    └──┘ └┘└───────────────┘└┘
typ    └──┘└┘└───────────────┘└┘
doc    └──┘ └┘                 └┘
txt    └──┘ └┘                 └┘
par    └──┘ └┘                 └┘
pid      └┘ └┘                 
st   ──────┘└─────────────────┘
836  end
st   └─┘
837  
838  noncomputable def nat_embedding (α : Type*) [infinite α] : ℕ ↪ α :=
id                                                └──────┘       
src                                               └──────┘       
typ                                               └──────┘       
839  ⟨_, nat_embedding_aux_injective α⟩
id       └─────────────────────────┘ 
src      └─────────────────────────┘
typ      └─────────────────────────┘ 
840  
841  end infinite
842  
843  lemma not_injective_infinite_fintype [infinite α] [fintype β] (f : α → β) :
id                                         └──────┘    └─────┘           
src                                        └──────┘     └─────┘
typ                                        └──────┘    └─────┘           
doc                                                     └─────┘
844    ¬ injective f :=
id      └───────┘ 
src     └───────┘
typ     └───────┘ 
845  assume (hf : injective f),
id                └───────┘ 
src               └───────┘
typ               └───────┘ 
846  have H : fintype α := fintype.of_injective f hf,
id            └─────┘     └──────────────────┘  └┘
src           └─────┘      └──────────────────┘
typ           └─────┘     └──────────────────┘  └┘
doc           └─────┘
847  infinite.not_fintype H
id   └──────────────────┘ 
src  └──────────────────┘
typ  └──────────────────┘ 
848  
849  lemma not_surjective_fintype_infinite [fintype α] [infinite β] (f : α → β) :
id                                          └─────┘    └──────┘           
src                                         └─────┘     └──────┘
typ                                         └─────┘    └──────┘           
doc                                         └─────┘
850    ¬ surjective f :=
id      └────────┘ 
src     └────────┘
typ     └────────┘ 
851  assume (hf : surjective f),
id                └────────┘ 
src               └────────┘
typ               └────────┘ 
852  have H : infinite α := infinite.of_surjective f hf,
id            └──────┘     └────────────────────┘  └┘
src           └──────┘      └────────────────────┘
typ           └──────┘     └────────────────────┘  └┘
853  @infinite.not_fintype _ H infer_instance
id    └──────────────────┘    └────────────┘
src   └──────────────────┘     └────────────┘
typ   └──────────────────┘    └────────────┘
doc                            └────────────┘
854  
855  instance nat.infinite : infinite ℕ :=
id                           └──────┘ 
src                          └──────┘ 
typ                          └──────┘ 
856  ⟨λ ⟨s, hs⟩, finset.not_mem_range_self $ s.subset_range_sup_succ (hs _)⟩
id        └┘   └───────────────────────┘    └────────────────────┘
src              └───────────────────────┘    └────────────────────┘
typ       └┘   └───────────────────────┘    └────────────────────┘
857  
858  instance int.infinite : infinite ℤ :=
id                           └──────┘ 
src                          └──────┘ 
typ                          └──────┘ 
859  infinite.of_injective int.of_nat (λ _ _, int.of_nat_inj)
id   └───────────────────┘ └────────┘       └────────────┘
src  └───────────────────┘ └────────┘         └────────────┘
typ  └───────────────────┘ └────────┘       └────────────┘